Efficient Representation and Validation of Proofs
George C. Necula and Peter Lee

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 allow the easy validation of properties of
safety-critical or untrusted code.

Our framework, which we call LFi, inherits from LF the capability to
encode various logics in a natural way. In addition, the LFi framework
allows proof representations without the high degree of redundancy
that is characteristic of LF representations. The missing parts of LFi
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
LFi instead of LF can make the difference between practically useless
proofs of several megabytes and manageable proofs of tens of
kilobytes.

The LICS paper is an abbreviated version of a longer (70 pages) technical
report. Read it if you want to see the detailed (15 pages) proofs of
soundness of the efficient proof-checking algorithm that is used in
PCC.