Towards a broad spectrum proof certificate
39 Pages
English
Gain access to the library to view online
Learn more

Towards a broad spectrum proof certificate

-

Gain access to the library to view online
Learn more
39 Pages
English

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


Subjects

Informations

Published by
Reads 3
Language English

Exrait

TowardsabroadspectrumproofcertificateDaleMillerINRIA-Saclay&LIX,E´colePolytechniquePalaiseau,FranceCarnegieMellonUniversity,17October2011Canwestandardize,communicate,andtrustformalproofs?
OutlineAboutformalproofsquicklyFourdesiderataforproofcertificatesMorespecificsaboutlogic,computation,andSometechnicalbits:Focusedproofsystemsfoorp
WemustfirstnarrowourtopicProofsaredocumentsthatareusedtocommunicatetrustwithinacommunityofagents.Agentscanbemachinesandhumans.Ourfocus:publishingandcheckingformalproofsbycomputeragentsNotourfocustoday:learningfromproofs,interactingwithproofs,computewithproofs.