An Information System Interpretation of Martin-Löf's Partial Type Theory with Universes

Erik Palmgren, Information and Computation 106(1993), 26 - 60.

Abstract. Martin-Löf's partial type theory, i.e. type theory with a fixed point operator, is extended with universes and given a domain-theoretic interpretation using Scott's information systems. The dependent types are interpreted as monotone families (parametrizations) of information systems and elements as relativized approximable mappings. Universes are interpreted as fixed points of the continuous operators (on the class of parametrizations) that are induced by the introduction rules for universes. Partial type theory has a rich type structure. In fact, as is shown elsewhere, Martin-Löf's inconsistent type theory, Type:Type, is definable in it. However, in this paper we give a direct interpretation of (an extension of) Type:Type as an application of the domain-theoretic method of solving type universe equations introduced here.

Back to the list of publications.

Erik Palmgren, March 9, 1999.