Proof Irrelevance and Strict Definitions in a Logical Framework
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.