## Paper: Efficient Representation and Validation of Proofs (at LICS 1998)

**George C. Necula Peter Lee**

### Abstract

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

### BibTeX

@InProceedings{NeculaLee-EfficientRepresenta, author = {George C. Necula and Peter Lee}, title = {Efficient Representation and Validation of Proofs}, booktitle = {Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science (LICS 1998)}, year = {1998}, month = {June}, pages = {93--104}, location = {Indianapolis, IN, USA}, publisher = {IEEE Computer Society Press} }