Domain interpretations of Martin-Löf's partial type theory (Q916656)

The Martin-Löf type theory considered is a monomorphic version, i.e. all type information is included in the terms, with the intensional identity type and containing a fixed point operator but not containing universes. On the domain side, the category DOM is considered, consisting of consistently complete algebraic cpo's with projection pairs as morphisms or, rather, effective such in terms of recursive enumeration theory. Each context \(\Gamma\) is interpreted as an effective domain \([[\Gamma]]\), each (dependent) type A in the context \(\Gamma\) is interpreted as an effective continuous functor \([[A]]_{\Gamma}: [[\Gamma]]\to DOM\) and each element \(a\in A\) in the context \(\Gamma\) is interpreted as an effective continuous function \([[a]]_{\Gamma}\) over \([[A]]_{\Gamma}\). Equality is interpreted as set theoretic equality. Two interpretations are given, one of which is shown to be adequate for the operational semantics of type theory in the sense that a closed term a terminates iff \([[a]]=\perp\). The interpretation has been modified and extended to type theory including universes in another paper of the first author [A domain interpretation of Martin-Löf's partial type theory with one universe, U.U.D.M. Report (1989)].