A type-theoretic interpretation of constructive domain theory

We present an interpreation of a constructive domain theory in Martin-Löf's type theory. More specifically, we construct a well-pointed Cartesian closed category of semilattices and approximable mappings. This construction is completely formalized and checked using the interactive proof assistant ALF. We base our work on Martin-Löf's domain interpretation of the theory of expressions underlying type theory. But our emphasis is different from Martin-Löf's, who interprets the program forms of type theory and proves a correspondence between their denotational and operational semantics. We instead show that a theory of domains can be developed within a well-defined fragment of (total) type theory. This is an important step toward constructing a model of all of partial type theory (type theory extended with general recursion) inside total type theory.