Proof Irrelevance and Strict Definitions in a Logical Framework

Jason Reed

June 2002

Senior Thesis

CMU-CS-02-153.ps
CMU-CS-02-153.pdf

Keywords: Proof irrelevance, type theory, LF, logical frameworks, dependent types, strictness, proof compression

The addition of proof irrelevant types to LF permits more expressive encodings and a richer (but still decidable) de nitional equality. These types can also be used to maintain invariants concerning the interchangeability of subproofs of large proofs, which can be useful for proof compression for proof-carrying code. We investigate the metatheoretic properties of this language extension and reconcile it with the notion of strictness, a property of notational definitions which can improve implementation efficiency of proofchecking.

56 pages