Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

Communicating and trusting proofs: The case for foundational proof certificates

Dale Miller 1, 2 
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : It is well recognized that proofs serve two different goals. On one hand, they can serve the didactic purpose of explaining why a theorem holds: that is, a proof has a message that is meant to describe the ''why'' behind a theorem. On the other hand, proofs can serve as certificates of validity. In this case, once a certificate is checked for its syntactic correctness, one can then trust that the theorem is, in fact, true. In this paper, we argue that structural proof theory and computer automation have matured to such a level that they can be used to provide a flexible and universal approach to proof-as-certificate. In contrast, the notion of proof-as-message is still evolving and deals with structures, such as diagrams and natural language texts, that are not yet well formalized.
Document type :
Preprints, Working Papers, ...
Complete list of metadata

Cited literature [35 references]  Display  Hide  Download
Contributor : Dale Miller Connect in order to contact the contributor
Submitted on : Friday, January 11, 2013 - 9:27:50 AM
Last modification on : Thursday, January 20, 2022 - 5:30:46 PM
Long-term archiving on: : Friday, April 12, 2013 - 11:16:34 AM


Files produced by the author(s)


  • HAL Id : hal-00772727, version 1



Dale Miller. Communicating and trusting proofs: The case for foundational proof certificates. 2013. ⟨hal-00772727⟩



Record views


Files downloads