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, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
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.
Type de document :
Communication dans un congrès
Chris Hawblitzel and Dale Miller. Second International Conference on Certified Programs and Proofs, Dec 2012, Kyoto, Japan. Springer, 7679, pp.208--223, 2012, Lecture Notes in Computer Science (LNCS). 〈10.1007/978-3-642-35308-6_17〉
Liste complète des métadonnées

Littérature citée [19 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00760118
Contributeur : Kaustuv Chaudhuri <>
Soumis le : lundi 3 décembre 2012 - 14:56:00
Dernière modification le : jeudi 10 mai 2018 - 02:06:41
Document(s) archivé(s) le : lundi 4 mars 2013 - 03:50:01

Fichiers

deepcert.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Kaustuv Chaudhuri. Compact Proof Certificates for Linear Logic. Chris Hawblitzel and Dale Miller. Second International Conference on Certified Programs and Proofs, Dec 2012, Kyoto, Japan. Springer, 7679, pp.208--223, 2012, Lecture Notes in Computer Science (LNCS). 〈10.1007/978-3-642-35308-6_17〉. 〈hal-00760118〉

Partager

Métriques

Consultations de la notice

432

Téléchargements de fichiers

127