Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, EpiSciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Conference papers

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
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.
Document type :
Conference papers
Complete list of metadata

Cited literature [21 references]  Display  Hide  Download
Contributor : Frédéric Blanqui Connect in order to contact the contributor
Submitted on : Wednesday, April 23, 2008 - 3:41:08 PM
Last modification on : Friday, January 21, 2022 - 3:14:05 AM
Long-term archiving on: : Friday, May 28, 2010 - 5:23:09 PM


Files produced by the author(s)




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. ⟨10.1007/978-0-387-09680-3_24⟩. ⟨inria-00275382⟩



Record views


Files downloads