Proof Irrelevance and Strict Definitions in a Logical Framework

Résumé du livre

Abstract: "The addition of proof irrelevant types to LF permits more expressive encodings and a richer (but still decidable) definitional 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."