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

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