Carnegie Mellon University
Browse

Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory

Download (106.81 kB)
journal contribution
posted on 1987-01-01, 00:00 authored by Frank Pfenning
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 α-conversion), extensionally (subject also to βη-conversion), or as irrelevant (equal to any other object at the same type), depending on where it occurs. Modal restrictions developed by R. Harper et al. (2000) for single 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, distinguished propositions (whose proofs are all identified - only their existence is important) from specifications (whose implementations are subject to some definitional equalities)

History

Publisher Statement

All Rights Reserved

Date

1987-01-01

Usage metrics

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC