|
CMU-CS-01-116
Computer Science Department
School of Computer Science, Carnegie Mellon University
CMU-CS-01-116
Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory
Frank Pfenning
April 2001
CMU-CS-01-.ps
CMU-CS-01-.pdf
Keywords: Logical frameworks, type theory, modal logic
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
beta-eta-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).
pages
|