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.