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

https://hal.inria.fr/hal-00772727
Contributor : Dale Miller <>
Submitted on : Friday, January 11, 2013 - 9:27:50 AM
Last modification on : Thursday, January 7, 2021 - 3:40:14 PM
Long-term archiving on: : Friday, April 12, 2013 - 11:16:34 AM

File

fpc.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00772727, version 1

Collections

Citation

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

Share

Metrics

Record views

458

Files downloads

190