@inproceedings{29e09125c90845b5a66463ba8d9a11c3,
title = "From formal proofs to mathematical proofs: A safe, incremental way for building in first-order decision procedures",
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.",
author = "Fr{\'e}deric Blanqui and Jouannaud, \{Jean Pierre\} and Strub, \{Pierre Yves\}",
year = "2008",
month = jan,
day = "1",
doi = "10.1007/978-0-387-09680-3\_24",
language = "English",
isbn = "9780387096797",
series = "IFIP International Federation for Information Processing",
publisher = "Springer New York",
pages = "349--365",
booktitle = "Fifth Ifip International Conference On Theoretical Computer Science - Tcs 2008",
}