A Proposal for Broad Spectrum Proof Certificates

Dale Miller

Description

Niveau: Supérieur
A Proposal for Broad Spectrum Proof Certificates Dale Miller INRIA-Saclay & LIX, Ecole Polytechnique Palaiseau, France Certified Programs and Proofs, 7 December 2011 Can we standardize, communicate, and trust formal proofs?

• might mean


• broad spectrum


• trust within


• checking formal


• focused proof


• proof certificates


• provers should

Sujets

• École polytechnique
• Broad-spectrum antibiotic

Informations

• Publié par: chaeh
• Nombre de lectures: 46
• Langue: English

Extrait

AProposalforBroadSpectrumProofCertificates DaleMiller INRIA-Saclay&LIX,E ´ colePolytechnique Palaiseau,France CertifiedProgramsandProofs,7December2011 Canwestandardize,communicate,andtrustformalproofs?

First,wenarrowourtopic Proofsaredocumentsthatareusedtocommunicatetrust withinacommunityofagents(humansandmachines). Proofcertificatesaredocumentsthatshoulddenoteproofs. Ourfocustoday: 1.Publishingandcheckingformalproofsbycomputeragents 2.Separateproofsfromprovenance. 3.Flexiblecertificatevssimplecheckers Notourfocustoday: 1.Humansandproofs:learningandinteractingwithproofs 2.DoIhavetherighttheorem? 3.etc.

Outline Fourdesiderataforproofcertificates Morespecificsaboutlogic,computation,and Thetechnicalbits:Focusedproofsystems rpfoo