Paper: Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory (at LICS 2001)

Authors: Frank Pfenning

Abstract

We develop a uniform type theory that integrates intensionality, extensionality, and proof irrelevance as judgmental concepts. Any object may be treated intensionally (subject only to alpha-conversion), extensionally (subject also to betaeta-conversion), or as irrelevant (equal to any other object at the same type), depending on where it occurs. Modal restrictions developed in prior work for simple types are generalized and employed to guarantee consistency between these views of objects. Potential applications are in logical frameworks, functional programming, and the foundations of first-order modal logics. Our type theory contrasts with previous approaches that a priori distinguish propositions (whose proofs are all identified-only their existence is important) from specifications (whose implementations are subject to some definitional equalities).

BibTeX

  @InProceedings{Pfenning-IntensionalityExten,
    author = 	 {Frank Pfenning},
    title = 	 {Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory},
    booktitle =  {Proceedings of the Sixteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2001)},
    year =	 {2001},
    month =	 {June}, 
    pages =      {221--230},
    location =   {Boston, MA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }