Compact Proof Certificates for Linear Logic - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2012

Compact Proof Certificates for Linear Logic

Résumé

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.
Fichier principal
Vignette du fichier
deepcert.pdf (191.71 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00760118 , version 1 (03-12-2012)

Identifiants

Citer

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⟩
226 Consultations
146 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More