
CMUCS97172
Computer Science Department
School of Computer Science, Carnegie Mellon University
CMUCS97172
Efficient Representation and Validation of Logical Proofs
George C. Necula, Peter Lee
October 1997
CMUCS97172.ps
CMUCS97172.ps.gz
Keywords: Proof representation, proof checking, logical frameworks,
type reconstruction, predicate logic, explicit substitutions, unification,
occurscheck optimization, proofcarrying code
This report describes a framework for representing and validating
formal proofs in various axiomatic systems. The framework is based on the
Edinburgh Logical Framework (LF) but is optimized for minimizing the size of
proofs and the complexity of proof validation, by removing redundant
representation components. Several variants of representation algorithms are
presented with the resulting representations being a factor of 15 smaller than
similar LF representations. The validation algorithm is a reconstruction
algorithm that runs about 7 times faster than LF typechecking. We present a
full proof of correctness of the reconstruction algorithm and hints for the
efficient implementation using explicit substitutions. We conclude with a
quantitative analysis of the algorithms.
72 pages
