Towards a broad spectrum proof certificate

Dale Miller

Description

Niveau: Supérieur
Towards a broad spectrum proof certificate Dale Miller INRIA-Saclay & LIX, Ecole Polytechnique Palaiseau, France Carnegie Mellon University, 17 October 2011 Can we standardize, communicate, and trust formal proofs?

• produce proofs


• between provers


• trust within


• checking formal


• focused proof


• another prover


• proofs quickly


• proof certificate


• exception when

Sujets

• École polytechnique

Informations

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

Extrait

Towardsabroadspectrumproofcertificate DaleMiller INRIA-Saclay&LIX,E ´ colePolytechnique Palaiseau,France CarnegieMellonUniversity,17October2011 Canwestandardize,communicate,andtrustformalproofs?

Outline Aboutformalproofsquickly Fourdesiderataforproofcertificates Morespecificsaboutlogic,computation,and Sometechnicalbits:Focusedproofsystems foorp

Wemustfirstnarrowourtopic Proofsaredocumentsthatareusedtocommunicatetrust withinacommunityofagents. Agentscanbemachinesandhumans. Ourfocus: publishingandcheckingformalproofsbycomputeragents Notourfocustoday:learningfromproofs,interactingwithproofs, computewithproofs.