A Type-Theoretic Interpretation of Constructive Domain Theory

Author: Hedberg M.

Source: Journal of Automated Reasoning, Volume 16, Number 3, June 1996 , pp. 369-425(57)

Publisher: Springer

Buy & download fulltext article:

Price: $47.00 plus tax (Refund Policy)

Abstract:

We present an interpretation 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. \null\hspace2mmWe 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.

Keywords: domains; Cartesian closure; type theory

Language: English

Document Type: Regular paper

Affiliations: 1: Programming Methodology Group, Department of Computing Science, University of Göteborg/Chalmers University of Technology, S-412 96 Göteborg, Sweden

Publication date: 1996-06-01