IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Thirteenth Annual IEEE Symposium on

Logic in Computer Science (LICS 1998)

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

Authors: George C. Necula 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 support 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


    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}

Last modified: 2017-04-0512:37
Andrzej Murawski