From formal proofs to mathematical proofs: a safe, incremental way for building in first-order decision procedures

Frédéric Blanqui 1, 2 Jean-Pierre Jouannaud 3, 4 Pierre-Yves Strub 3, 4
1 FORMES - Formal Methods for Embedded Systems
LIAMA - Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées, Inria Paris-Rocquencourt
2 PAREO - Formal islands: foundations and applications
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
3 LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
4 TYPICAL - Types, Logic and computing
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : We investigate here a new version of the Calculus of Inductive Constructions (CIC) on which the proof assistant Coq is based: the Calculus of Congruent Inductive Constructions, which truly extends CIC by building in arbitrary first-order decision procedures: deduction is still in charge of the CIC kernel, while computation is outsourced to dedicated first-order decision procedures that can be taken from the shelves provided they deliver a proof certificate. The soundness of the whole system becomes an incremental property following from the soundness of the certificate checkers and that of the kernel. A detailed example shows that the resulting style of proofs becomes closer to that of the working mathematician.
Keywords : proof assistants proof lambda-calculus calculus of constructions certification decision procedures first-order theory type theory
Type de document :
Communication dans un congrès
5th IFIP International Conference on Theoretical Computer Science - TCS 2008, Sep 2008, Milan, Italy. 273, 2008, IFIP. 〈10.1007/978-0-387-09680-3_24〉
Liste complète des métadonnées

Littérature citée [21 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/inria-00275382
Contributeur : Frédéric Blanqui <>
Soumis le : mercredi 23 avril 2008 - 15:41:08
Dernière modification le : mercredi 14 novembre 2018 - 15:30:04
Document(s) archivé(s) le : vendredi 28 mai 2010 - 17:23:09

Fichiers

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

Identifiants

Collections

INRIA | LIX | LIAMA | X-LIX | X | PARISTECH | INRA | CIRAD | LORIA | UNIV-LORRAINE | INRIA-ROCQ | X-DEP-INFO

Citation

Frédéric Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub. From formal proofs to mathematical proofs: a safe, incremental way for building in first-order decision procedures. 5th IFIP International Conference on Theoretical Computer Science - TCS 2008, Sep 2008, Milan, Italy. 273, 2008, IFIP. 〈10.1007/978-0-387-09680-3_24〉. 〈inria-00275382〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

687

Téléchargements de fichiers

163

Contact


archive-ouverte@inria.fr