Carnegie Mellon University
Browse

Refinement Types as Proof Irrelevance

Download (190.99 kB)
journal contribution
posted on 2011-06-01, 00:00 authored by William Lovas, Frank Pfenning
Refinement types sharpen systems of simple and dependent types by offering expressive means to more precisely classify well-typed terms. Proof irrelevance provides a mechanism for selectively hiding the identities of terms in type theories. In this paper, we show that refinement types can be interpreted as predicates using proof irrelevance in the context of the logical framework LF, establishing a uniform relationship between two previously studied concepts in type theory. The interpretation and its correctness proof are surprisingly complex, lending credence to the idea that refinement types are a fundamental construct rather than just a convenient surface syntax for certain uses of proof irrelevance.

History

Publisher Statement

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-642-29963-6_5

Date

2011-06-01

Usage metrics

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC