## Paper: On computational open-endedness in Martin-Lof's type theory (at LICS 1991)

**Douglas J. Howe**

### Abstract

Computational open-endedness in a type theory is defined as the property that theorems remain true under extensions to the underlying programming language. Some properties related to open-endedness that are relevant to machine implementations of type theory are established. A class of computation systems, specified by a simple but fairly general kind of structural operational semantics, with respect to which P. Martin-Lof's (6th Int. Congress for Logic, Methodology, and Philosophy of Science, p.153-175, 1982) type theory (and most of its descendants) is open-ended is defined. It is shown that any such system validates a useful form of type free reasoning about program equivalence and that symbolic computation procedures can be automatically derived from these specifications. The main result is the definition of a particular computation system that includes a collection of oracles sufficient to provide a classical semantics for Martin-Lof's type theory in which the excluded middle law holds

### BibTeX

@InProceedings{Howe-Oncomputationalopen, author = {Douglas J. Howe}, title = {On computational open-endedness in Martin-Lof's type theory}, booktitle = {Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science (LICS 1991)}, year = {1991}, month = {July}, pages = {162--172}, location = {Amsterdam, The Netherlands}, publisher = {IEEE Computer Society Press} }