Communicating and trusting proofs: The case for foundational proof certificates

Dale Miller 1, 2
1 PARSIFAL - Proof search and reasoning with logic specifications
Inria Saclay - Ile de France, LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
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.
Type de document :
Pré-publication, Document de travail
To appear in the Proceedings of the 14th Congress of Logic, Methodology and Philosophy of Science.. 2013
Liste complète des métadonnées

Littérature citée [35 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00772727
Contributeur : Dale Miller <>
Soumis le : vendredi 11 janvier 2013 - 09:27:50
Dernière modification le : mercredi 14 novembre 2018 - 16:14:01
Document(s) archivé(s) le : vendredi 12 avril 2013 - 11:16:34

Fichier

fpc.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00772727, version 1

Collections

Citation

Dale Miller. Communicating and trusting proofs: The case for foundational proof certificates. To appear in the Proceedings of the 14th Congress of Logic, Methodology and Philosophy of Science.. 2013. 〈hal-00772727〉

Partager

Métriques

Consultations de la notice

353

Téléchargements de fichiers

140