登入選單

返回Google圖書搜尋

Proof Irrelevance and Strict Definitions in a Logical Framework

Jason Reed

出版	School of Computer Science, Carnegie Mellon University, 2002
URL	http://books.google.com.hk/books?id=mHcwHQAACAAJ&hl=&source=gbs_api

註釋

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."