Lics

IEEE Symposium on Logic in Computer Science

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

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}
 }