## 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.