George C. Necula, Peter Lee
CMU
Efficient Representation and Validation of Proofs
Presented at LICS'98.
URL: http://raw.cs.berkeley.edu/Papers/lfi_lics98.ps
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.
|