Skip to Main content Skip to Navigation
New interface
Conference papers

Compact Proof Certificates for Linear Logic

Kaustuv Chaudhuri 1 
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : Linear logic is increasingly being used as a tool for communicating reasoning agents in domains such as authorization, access control, electronic voting, etc., where proof certificates represent evidence that must be verified by proof consumers as part of higher protocols. Controlling the size of these certificates is critical. We assume that the proof consumer is allowed to do some search to reconstruct details of the full proof that are omitted from the certificates. Because the decision problem for linear logic is unsolvable, the certificate must contain at least enough information to bound the search: we show how to use the sequence of contractions in the sequent proof for this bound. The remaining content of the proof, in particular the information about resource divisions, can then be omitted from the certificate. We also describe a technique for giving a variable amount of additional search hints to the proof consumer to limit its non-determinism.
Document type :
Conference papers
Complete list of metadata

Cited literature [19 references]  Display  Hide  Download
Contributor : Kaustuv Chaudhuri Connect in order to contact the contributor
Submitted on : Monday, December 3, 2012 - 2:56:00 PM
Last modification on : Thursday, January 20, 2022 - 5:30:46 PM
Long-term archiving on: : Monday, March 4, 2013 - 3:50:01 AM


Files produced by the author(s)




Kaustuv Chaudhuri. Compact Proof Certificates for Linear Logic. Second International Conference on Certified Programs and Proofs, Dec 2012, Kyoto, Japan. pp.208--223, ⟨10.1007/978-3-642-35308-6_17⟩. ⟨hal-00760118⟩



Record views


Files downloads