Is there a good notion of non-termination and halting proofs in type theory? Constructive type theory with its basic interpretation under the curry howard correspondence consists only of total, computable functions. In the literature, some has been said on using "computational type theory" in order to represent non-termination in functional programs, yet in the papers I have come across, this does not seem to be the major motivation for the theory (For example Benton mentions non-determinism, continuations, and exceptions, without going into much detail on non-termination), so I have yet to find a paper giving a robust interpretation of non-termination using computational type theory.

Specifically, what I am looking for is a way that given a type representing a possibly non terminating computation of type $A$, $T(A)$, there should be some notion of proofs that $x : T(A)$ terminates of type $H(x)$, such that given $x:T(A)$ and $p:H(x)$, we can construct a term $\tilde x : A$. 

My motivation for this is, I'd like to eventually be able to more formally relate notions in computational complexity theory to constructive type theory. Specifically, I am interested in what power as a formal theory constructive types gain with access to a halting oracle, and in order to do so, I of course need to actually have a formal notion of possible non-termination, and proofs of halting to go along with it inside a type-theoretic framework.
Because one of the principal applications of Type Theory in formalizations has been to study programing languages and computation in general, a lot of thought has gone into ways of representing possibly non-terminating programs.

I won't make a complete survey here, but I'll try and give pointers to the main thrusts of different directions.


The "relational" approach: you can define your hypothetical programs as relations say, $F\ x\ y$ which holds iff $f$ is defined at $x$ and $f(x)=y$. This is usually what is done with the Kleene T-predicate. This works just as well in type theory formalizations as it does in classical logic, (though of course you can't prove $\forall x (\exists y, F\ x\ y)\vee (\neg\exists y, F\ x\ y)$).

A more sophisticated way to do this is the "Bove-Capretta" method (see Modelling Recursion in Type Theory, which for each recursive function, defines an "accessible predicate" which encodes the fact that a given computation is finite. The function definition takes an extra argument which is a proof that the given inputs are accessible. To define the function without this extra predicate, you need to prove that every possible combination of inputs is accessible.
The "coinductive" approach: this is possibly the most explored approach, and what Andrej's comments refer to. A computation of type $A$ is defined as the inductive type (from Andrej's link, by Capretta, Altenkirch &amp; Uustalu:

codata Delay A =
| Now : A -&gt; Delay A
| Later (Delay A)


This codes a possibly infinite stream of Later tokens ("ticks" of computation) maybe ending with a result Now a. Non-termination is equivalent to being bisimilar with the program

loop = Later loop
and termination can be defined by an inductive predicate over Delay A:

data Terminates : Data A -&gt; Prop =
| Term_now : forall x, Terminates (Now x)
| Term_later : forall d, Terminates d -&gt; Terminates (Later d)


I think the agda-istas have a lot to say about this which they call the partiality monad (see e.g. Danielsson).
The "partial type theory" approach: this is a bit more experimental (the theory is still being worked out), but there are some type theories that are being developed to cope with the fact that there are essentially two types of functions we want to write in type theory: the proof terms and the programs. It turns out to be tough to get a reasonable theory of these things (and retain consistency of the theory), but a serious attempt is made here by Casinghino et al, and a similar effort by Kimmel et al.


I'm sure there are other approaches I'm not aware of, and I'd be happy if someone wants to complete this list.

I should probably note that adding a termination oracle to a (consistent) type theory is a lot like adding a truth oracle for $\Pi^0_1$ sentences, with relatively well understood consequences.

There are other, quite fruitful interactions between type theory and complexity theory, usually under the umbrella of implicit computational complexity.