## Paper: A Non-Type-Theoretic Definition of Martin-Löf's Types (at LICS 1987)

**Stuart F. Allen**

### Abstract

It is possible to make a natural non-type-theoretic
reinterpretaion of Martin-Löfs type theory. This paper presents an inductive
definition of the types explicitly defined in Martin-Löf'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-Löf'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.

### BibTeX

@InProceedings{Allen-ANonTypeTheoreticDe, author = {Stuart F. Allen}, title = {A Non-Type-Theoretic Definition of Martin-Löf's Types}, booktitle = {Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science (LICS 1987)}, year = {1987}, month = {June}, pages = {215--221 }, location = {Ithaca, NY, USA}, publisher = {IEEE Computer Society Press} }