A Non-Type-Theoretic Definition of Martin-Löf's Types

Stuart Allen

Tech Report, Cornell University


based on LICS'87 Proceedings


It is possible to make a natural non-type-theoretic reinterpretation of Martin-Lof's type theory. This paper presents an inductive definition of the types explicitly defined in Martin-Lof's paper, Constructive Mathematics and Computer Programming. The definition is set-theoretically valid, and probably will be convincing to intuitionists as well. When this definition is used with methods set out in the author's thesis, the inference rules presented in Martin-Lof's paper can be shown to be valid under the non-type-theoretic interpretation. This interpretation is non-trivial, that is, there are both inhabited types and empty types, and so, validity entails simple consistency. Finally, Michael Beeson has defined some recursive realizability models which we shall compare with the term model presented here, and we shall compare the methods of definition.

Section Headings
Anatomy of the Type Constructors
Extensional Type Systems
The Inductive Definition
Adequacy of the Definition
Formal Proof -- Consistency
Comparison with Beeson's Recursive Models

This paper was presented at LICS'87 and slightly altered as Cornell CS Department Tech Report TR87-832.

A postscript version of the Tech Report reset for better legibility is TR87-832-RESET.ps

The official version of the Tech Report appears to be an OCR scanned version
and is available at http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR87-866

The LICS'87 version, but reset with different pagination, is LICS87sfa.ps

See also A Non-Type-Theoretic Semantics for Type-Theoretic Language.
Back to PRL Project Publications.