Skip to Main content Skip to Navigation
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

https://hal.inria.fr/hal-00760118
Contributor : Kaustuv Chaudhuri <>
Submitted on : Monday, December 3, 2012 - 2:56:00 PM
Last modification on : Thursday, January 7, 2021 - 3:40:14 PM
Long-term archiving on: : Monday, March 4, 2013 - 3:50:01 AM

Files

deepcert.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

569

Files downloads

394