From formal proofs to mathematical proofs: a safe, incremental way for building in first-order decision procedures
Identifieur interne : 002485 ( Hal/Corpus ); précédent : 002484; suivant : 002486From formal proofs to mathematical proofs: a safe, incremental way for building in first-order decision procedures
Auteurs : Frédéric Blanqui ; Jean-Pierre Jouannaud ; Pierre-Yves StrubSource :
English descriptors
- mix :
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.
Url:
DOI: 10.1007/978-0-387-09680-3_24
Links to Exploration step
Hal:inria-00275382Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en">From formal proofs to mathematical proofs: a safe, incremental way for building in first-order decision procedures</title><author><name sortKey="Blanqui, Frederic" sort="Blanqui, Frederic" uniqKey="Blanqui F" first="Frédéric" last="Blanqui">Frédéric Blanqui</name><affiliation><hal:affiliation type="researchteam" xml:id="struct-85226" status="OLD"><idno type="RNSR">200921233V</idno><orgName>Formal Methods for Embedded Systems</orgName><orgName type="acronym">FORMES</orgName><desc><address><addrLine>Tsinghua University FIT Building Haidian District 100084 Beijing China</addrLine><country key="CN"></country></address><ref type="url">http://liama.ia.ac.cn/wiki/projects:formes:home</ref></desc><listRelation><relation active="#struct-25361" type="direct"></relation><relation active="#struct-11574" type="indirect"></relation><relation active="#struct-92114" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-300133" type="indirect"></relation><relation active="#struct-300168" type="indirect"></relation><relation active="#struct-441569" type="indirect"></relation><relation active="#struct-86790" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-25361" type="direct"><org type="laboratory" xml:id="struct-25361" status="VALID"><orgName>Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées</orgName><orgName type="acronym">LIAMA</orgName><desc><address><addrLine>Institut d'Automatique - Académie des Sciences de Chine PO Box 2728 - Beijing 100080 R. P. Chine Tél. : (+ 86 10) 62 64 74 59 Fax : (+ 86 10) 62 64 74 58</addrLine><country key="CN"></country></address><ref type="url">http://liama.ia.ac.cn/</ref></desc><listRelation><relation active="#struct-11574" type="direct"></relation><relation active="#struct-92114" type="direct"></relation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-300133" type="direct"></relation><relation active="#struct-300168" type="direct"></relation><relation active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-11574" type="indirect"><org type="institution" xml:id="struct-11574" status="VALID"><orgName>Centre de Coopération Internationale en Recherche Agronomique pour le Développement</orgName><orgName type="acronym">CIRAD</orgName><desc><address><addrLine>42, rue Scheffer 75116 Paris</addrLine><country key="FR"></country></address><ref type="url">http://www.cirad.fr</ref></desc></org></tutelle><tutelle active="#struct-92114" type="indirect"><org type="institution" xml:id="struct-92114" status="VALID"><orgName>Institut National de la Recherche Agronomique</orgName><orgName type="acronym">INRA</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inra.fr</ref></desc></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-300133" type="indirect"><org type="institution" xml:id="struct-300133" status="VALID"><orgName>Chinese Academy of Science (CAS)</orgName><desc><address><country key="CN"></country></address></desc></org></tutelle><tutelle active="#struct-300168" type="indirect"><org type="institution" xml:id="struct-300168" status="VALID"><orgName>Institute of Automation, Chinese Academy of Sciences</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-86790" type="direct"><org type="laboratory" xml:id="struct-86790" status="VALID"><idno type="RNSR">196718247G</idno><orgName>INRIA Paris-Rocquencourt</orgName><desc><address><addrLine>INRIA Rocquencourt : Domaine de Voluceau, Rocquencourt B.P. 105 78153 le Chesnay Cedex / INRIA Paris - 23 avenue d'Italie 75013 Paris</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/centre/paris-rocquencourt</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle></tutelles></hal:affiliation></affiliation></author><author><name sortKey="Jouannaud, Jean Pierre" sort="Jouannaud, Jean Pierre" uniqKey="Jouannaud J" first="Jean-Pierre" last="Jouannaud">Jean-Pierre Jouannaud</name><affiliation><hal:affiliation type="laboratory" xml:id="struct-2071" status="VALID"><orgName>Laboratoire d'informatique de l'École polytechnique [Palaiseau]</orgName><orgName type="acronym">LIX</orgName><desc><address><addrLine>Route de Saclay 91128 PALAISEAU CEDEX</addrLine><country key="FR"></country></address><ref type="url">http://www.lix.polytechnique.fr/</ref></desc><listRelation><relation active="#struct-300340" type="direct"></relation><relation name="UMR7161" active="#struct-441569" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-300340" type="direct"><org type="institution" xml:id="struct-300340" status="VALID"><orgName>Polytechnique - X</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle name="UMR7161" active="#struct-441569" type="direct"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation></affiliation></author><author><name sortKey="Strub, Pierre Yves" sort="Strub, Pierre Yves" uniqKey="Strub P" first="Pierre-Yves" last="Strub">Pierre-Yves Strub</name><affiliation><hal:affiliation type="laboratory" xml:id="struct-2071" status="VALID"><orgName>Laboratoire d'informatique de l'École polytechnique [Palaiseau]</orgName><orgName type="acronym">LIX</orgName><desc><address><addrLine>Route de Saclay 91128 PALAISEAU CEDEX</addrLine><country key="FR"></country></address><ref type="url">http://www.lix.polytechnique.fr/</ref></desc><listRelation><relation active="#struct-300340" type="direct"></relation><relation name="UMR7161" active="#struct-441569" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-300340" type="direct"><org type="institution" xml:id="struct-300340" status="VALID"><orgName>Polytechnique - X</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle name="UMR7161" active="#struct-441569" type="direct"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">HAL</idno><idno type="RBID">Hal:inria-00275382</idno><idno type="halId">inria-00275382</idno><idno type="halUri">https://hal.inria.fr/inria-00275382</idno><idno type="url">https://hal.inria.fr/inria-00275382</idno><idno type="doi">10.1007/978-0-387-09680-3_24</idno><date when="2008-09-08">2008-09-08</date><idno type="wicri:Area/Hal/Corpus">002485</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">From formal proofs to mathematical proofs: a safe, incremental way for building in first-order decision procedures</title><author><name sortKey="Blanqui, Frederic" sort="Blanqui, Frederic" uniqKey="Blanqui F" first="Frédéric" last="Blanqui">Frédéric Blanqui</name><affiliation><hal:affiliation type="researchteam" xml:id="struct-85226" status="OLD"><idno type="RNSR">200921233V</idno><orgName>Formal Methods for Embedded Systems</orgName><orgName type="acronym">FORMES</orgName><desc><address><addrLine>Tsinghua University FIT Building Haidian District 100084 Beijing China</addrLine><country key="CN"></country></address><ref type="url">http://liama.ia.ac.cn/wiki/projects:formes:home</ref></desc><listRelation><relation active="#struct-25361" type="direct"></relation><relation active="#struct-11574" type="indirect"></relation><relation active="#struct-92114" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-300133" type="indirect"></relation><relation active="#struct-300168" type="indirect"></relation><relation active="#struct-441569" type="indirect"></relation><relation active="#struct-86790" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-25361" type="direct"><org type="laboratory" xml:id="struct-25361" status="VALID"><orgName>Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées</orgName><orgName type="acronym">LIAMA</orgName><desc><address><addrLine>Institut d'Automatique - Académie des Sciences de Chine PO Box 2728 - Beijing 100080 R. P. Chine Tél. : (+ 86 10) 62 64 74 59 Fax : (+ 86 10) 62 64 74 58</addrLine><country key="CN"></country></address><ref type="url">http://liama.ia.ac.cn/</ref></desc><listRelation><relation active="#struct-11574" type="direct"></relation><relation active="#struct-92114" type="direct"></relation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-300133" type="direct"></relation><relation active="#struct-300168" type="direct"></relation><relation active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-11574" type="indirect"><org type="institution" xml:id="struct-11574" status="VALID"><orgName>Centre de Coopération Internationale en Recherche Agronomique pour le Développement</orgName><orgName type="acronym">CIRAD</orgName><desc><address><addrLine>42, rue Scheffer 75116 Paris</addrLine><country key="FR"></country></address><ref type="url">http://www.cirad.fr</ref></desc></org></tutelle><tutelle active="#struct-92114" type="indirect"><org type="institution" xml:id="struct-92114" status="VALID"><orgName>Institut National de la Recherche Agronomique</orgName><orgName type="acronym">INRA</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inra.fr</ref></desc></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-300133" type="indirect"><org type="institution" xml:id="struct-300133" status="VALID"><orgName>Chinese Academy of Science (CAS)</orgName><desc><address><country key="CN"></country></address></desc></org></tutelle><tutelle active="#struct-300168" type="indirect"><org type="institution" xml:id="struct-300168" status="VALID"><orgName>Institute of Automation, Chinese Academy of Sciences</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-86790" type="direct"><org type="laboratory" xml:id="struct-86790" status="VALID"><idno type="RNSR">196718247G</idno><orgName>INRIA Paris-Rocquencourt</orgName><desc><address><addrLine>INRIA Rocquencourt : Domaine de Voluceau, Rocquencourt B.P. 105 78153 le Chesnay Cedex / INRIA Paris - 23 avenue d'Italie 75013 Paris</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/centre/paris-rocquencourt</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle></tutelles></hal:affiliation></affiliation></author><author><name sortKey="Jouannaud, Jean Pierre" sort="Jouannaud, Jean Pierre" uniqKey="Jouannaud J" first="Jean-Pierre" last="Jouannaud">Jean-Pierre Jouannaud</name><affiliation><hal:affiliation type="laboratory" xml:id="struct-2071" status="VALID"><orgName>Laboratoire d'informatique de l'École polytechnique [Palaiseau]</orgName><orgName type="acronym">LIX</orgName><desc><address><addrLine>Route de Saclay 91128 PALAISEAU CEDEX</addrLine><country key="FR"></country></address><ref type="url">http://www.lix.polytechnique.fr/</ref></desc><listRelation><relation active="#struct-300340" type="direct"></relation><relation name="UMR7161" active="#struct-441569" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-300340" type="direct"><org type="institution" xml:id="struct-300340" status="VALID"><orgName>Polytechnique - X</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle name="UMR7161" active="#struct-441569" type="direct"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation></affiliation></author><author><name sortKey="Strub, Pierre Yves" sort="Strub, Pierre Yves" uniqKey="Strub P" first="Pierre-Yves" last="Strub">Pierre-Yves Strub</name><affiliation><hal:affiliation type="laboratory" xml:id="struct-2071" status="VALID"><orgName>Laboratoire d'informatique de l'École polytechnique [Palaiseau]</orgName><orgName type="acronym">LIX</orgName><desc><address><addrLine>Route de Saclay 91128 PALAISEAU CEDEX</addrLine><country key="FR"></country></address><ref type="url">http://www.lix.polytechnique.fr/</ref></desc><listRelation><relation active="#struct-300340" type="direct"></relation><relation name="UMR7161" active="#struct-441569" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-300340" type="direct"><org type="institution" xml:id="struct-300340" status="VALID"><orgName>Polytechnique - X</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle name="UMR7161" active="#struct-441569" type="direct"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation></affiliation></author></analytic><idno type="DOI">10.1007/978-0-387-09680-3_24</idno></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="mix" xml:lang="en"><term>calculus of constructions</term><term>certification</term><term>decision procedures</term><term>first-order theory</term><term>lambda-calculus</term><term>proof</term><term>proof assistants</term><term>type theory</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">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.</div></front></TEI><hal api="V3"><titleStmt><title xml:lang="en">From formal proofs to mathematical proofs: a safe, incremental way for building in first-order decision procedures</title><author role="aut"><persName><forename type="first">Frédéric</forename><surname>Blanqui</surname></persName><email>blanqui@loria.fr</email><idno type="halauthor">303337</idno><affiliation ref="#struct-85226"></affiliation><affiliation ref="#struct-54175"></affiliation></author><author role="aut"><persName><forename type="first">Jean-Pierre</forename><surname>Jouannaud</surname></persName><email>jouannaud@lix.polytechnique.fr</email><idno type="halauthor">120659</idno><orgName ref="#struct-300340"></orgName><affiliation ref="#struct-2071"></affiliation><affiliation ref="#struct-55047"></affiliation></author><author role="aut"><persName><forename type="first">Pierre-Yves</forename><surname>Strub</surname></persName><email>strub@lix.polytechnique.fr</email><idno type="halauthor">193747</idno><orgName ref="#struct-300340"></orgName><affiliation ref="#struct-2071"></affiliation><affiliation ref="#struct-55047"></affiliation></author><editor role="depositor"><persName><forename>Frédéric</forename><surname>Blanqui</surname></persName><email>frederic.blanqui@inria.fr</email></editor></titleStmt><editionStmt><edition n="v1" type="current"><date type="whenSubmitted">2008-04-23 15:41:08</date><date type="whenModified">2016-05-18 08:55:13</date><date type="whenReleased">2008-04-23 18:56:55</date><date type="whenProduced">2008-09-08</date><date type="whenEndEmbargoed">2008-04-23</date><ref type="file" target="https://hal.inria.fr/inria-00275382/document"><date notBefore="2008-04-23"></date></ref><ref type="file" subtype="author" n="1" target="https://hal.inria.fr/inria-00275382/file/main.pdf"><date notBefore="2008-04-23"></date></ref></edition><respStmt><resp>contributor</resp><name key="102606"><persName><forename>Frédéric</forename><surname>Blanqui</surname></persName><email>frederic.blanqui@inria.fr</email></name></respStmt></editionStmt><publicationStmt><distributor>CCSD</distributor><idno type="halId">inria-00275382</idno><idno type="halUri">https://hal.inria.fr/inria-00275382</idno><idno type="halBibtex">blanqui:inria-00275382</idno><idno type="halRefHtml">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></idno><idno type="halRef">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></idno></publicationStmt><seriesStmt><idno type="stamp" n="CNRS">CNRS - Centre national de la recherche scientifique</idno><idno type="stamp" n="INRIA">INRIA - Institut National de Recherche en Informatique et en Automatique</idno><idno type="stamp" n="LIX">Laboratoire d'informatique de l'école polytechnique</idno><idno type="stamp" n="LIAMA">Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées</idno><idno type="stamp" n="X-LIX" p="X">Laboratoire d'informatique de l'X (LIX)</idno><idno type="stamp" n="X-DEP">Polytechnique</idno><idno type="stamp" n="X-DEP-INFO" p="X-DEP">Département d'informatique</idno><idno type="stamp" n="X" p="PARISTECH">Ecole Polytechnique</idno><idno type="stamp" n="PARISTECH">ParisTech</idno><idno type="stamp" n="INRIA-SACLAY">INRIA Saclay - Ile de France</idno><idno type="stamp" n="INPL">Institut National Polytechnique de Lorraine</idno><idno type="stamp" n="LORIA2">Publications du LORIA</idno><idno type="stamp" n="INRIA-NANCY-GRAND-EST">INRIA Nancy - Grand Est</idno><idno type="stamp" n="LORIA-FM" p="LORIA">Méthodes formelles</idno><idno type="stamp" n="LORIA">LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications</idno><idno type="stamp" n="INRIA2">INRIA 2</idno><idno type="stamp" n="INRA">INRA - Institut national de la recherche agronomique</idno><idno type="stamp" n="INRIA-LORRAINE">INRIA Nancy - Grand Est</idno><idno type="stamp" n="LABO-LORIA-SET" p="LORIA">LABO-LORIA-SET</idno><idno type="stamp" n="CIRAD">CIRAD - Centre de coopération internationale en recherche agronomique pour le développement</idno><idno type="stamp" n="INRIA_TEST">INRIA - Institut National de Recherche en Informatique et en Automatique</idno><idno type="stamp" n="UNIV-LORRAINE">Université de Lorraine</idno></seriesStmt><notesStmt><note type="audience" n="2">International</note><note type="invited" n="0">No</note><note type="popular" n="0">No</note><note type="peer" n="1">Yes</note><note type="proceedings" n="1">Yes</note></notesStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">From formal proofs to mathematical proofs: a safe, incremental way for building in first-order decision procedures</title><author role="aut"><persName><forename type="first">Frédéric</forename><surname>Blanqui</surname></persName><email>blanqui@loria.fr</email><idno type="halAuthorId">303337</idno><affiliation ref="#struct-85226"></affiliation><affiliation ref="#struct-54175"></affiliation></author><author role="aut"><persName><forename type="first">Jean-Pierre</forename><surname>Jouannaud</surname></persName><email>jouannaud@lix.polytechnique.fr</email><idno type="halAuthorId">120659</idno><orgName ref="#struct-300340"></orgName><affiliation ref="#struct-2071"></affiliation><affiliation ref="#struct-55047"></affiliation></author><author role="aut"><persName><forename type="first">Pierre-Yves</forename><surname>Strub</surname></persName><email>strub@lix.polytechnique.fr</email><idno type="halAuthorId">193747</idno><orgName ref="#struct-300340"></orgName><affiliation ref="#struct-2071"></affiliation><affiliation ref="#struct-55047"></affiliation></author></analytic><monogr><meeting><title>5th IFIP International Conference on Theoretical Computer Science - TCS 2008</title><date type="start">2008-09-08</date><settlement>Milan</settlement><country key="IT">Italy</country></meeting><imprint><biblScope unit="serie">IFIP</biblScope><biblScope unit="volume">273</biblScope><date type="datePub">2008</date></imprint></monogr><idno type="arxiv">0804.3762</idno><idno type="doi">10.1007/978-0-387-09680-3_24</idno></biblStruct></sourceDesc><profileDesc><langUsage><language ident="en">English</language></langUsage><textClass><keywords scheme="author"><term xml:lang="en">proof assistants</term><term xml:lang="en">proof</term><term xml:lang="en">lambda-calculus</term><term xml:lang="en">calculus of constructions</term><term xml:lang="en">certification</term><term xml:lang="en">decision procedures</term><term xml:lang="en">first-order theory</term><term xml:lang="en">type theory</term></keywords><classCode scheme="halDomain" n="info.info-lo">Computer Science [cs]/Logic in Computer Science [cs.LO]</classCode><classCode scheme="halTypology" n="COMM">Conference papers</classCode></textClass><abstract xml:lang="en">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.</abstract></profileDesc></hal></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Hal/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 002485 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Hal/Corpus/biblio.hfd -nk 002485 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Hal
|étape= Corpus
|type= RBID
|clé= Hal:inria-00275382
|texte= From formal proofs to mathematical proofs: a safe, incremental way for building in first-order decision procedures
}}
| This area was generated with Dilib version V0.6.33. |  |