Efficient representation and validation of proofs

This paper presents a logical framework derived from the Edinburgh Logical Framework (LF) that can be used to obtain compact representations of proofs and efficient proof checkers. These are essential ingredients of any application that manipulates proofs as first-class objects, such as a Proof-Carrying Code system, in which proofs are used to support easy validation of properties of safety-critical or untrusted code. Our framework, which we call LF_i , inherits from LF the capability to encode various logics in a natural way. In addition, the LF_i framework allows proof representations without the high degree of redundancy that is characteristic of LF representations. The missing parts of LF_i proof representations can be reconstructed during proof checking by an efficient reconstruction algorithm. We also describe an algorithm that can be used to strip the unnecessary parts of an LF representation of a proof. The experimental data that we gathered in the context of a Proof-Carrying Code system shows that the savings obtained from using LF_i instead of LF can make the difference between practically useless proofs of several megabytes and manageable proofs of tens of kilobytes