Proof Reflection in Coq
Identifieur interne : 000351 ( Istex/Curation ); précédent : 000350; suivant : 000352Proof Reflection in Coq
Auteurs : Dimitri HendriksSource :
- Journal of Automated Reasoning [ 0168-7433 ] ; 2002-09-01.
English descriptors
- KwdEn :
Abstract
Abstract: We formalize natural deduction for first-order logic in the proof assistant Coq, using de Bruijn indices for variable binding. The main judgment we model is of the form Γ⊢d [:] φ, stating that d is a proof term of formula φ under hypotheses Γ it can be viewed as a typing relation by the Curry–Howard isomorphism. This relation is proved sound with respect to Coq's native logic and is amenable to the manipulation of formulas and of derivations. As an illustration, we define a reduction relation on proof terms with permutative conversions and prove the property of subject reduction.
Url:
DOI: 10.1023/A:1021923116629
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: Pour aller vers cette notice dans l'étape Curation :000353
Links to Exploration step
ISTEX:0FB03B36445C9F881F41EAA2510FD268A48850CFLe document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Proof Reflection in Coq</title><author><name sortKey="Hendriks, Dimitri" sort="Hendriks, Dimitri" uniqKey="Hendriks D" first="Dimitri" last="Hendriks">Dimitri Hendriks</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:0FB03B36445C9F881F41EAA2510FD268A48850CF</idno><date when="2002" year="2002">2002</date><idno type="doi">10.1023/A:1021923116629</idno><idno type="url">https://api.istex.fr/ark:/67375/VQC-R56L80GL-1/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">000353</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000353</idno><idno type="wicri:Area/Istex/Curation">000351</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Proof Reflection in Coq</title><author><name sortKey="Hendriks, Dimitri" sort="Hendriks, Dimitri" uniqKey="Hendriks D" first="Dimitri" last="Hendriks">Dimitri Hendriks</name></author></analytic><monogr></monogr><series><title level="j">Journal of Automated Reasoning</title><title level="j" type="abbrev">Journal of Automated Reasoning</title><idno type="ISSN">0168-7433</idno><idno type="eISSN">1573-0670</idno><imprint><publisher>Kluwer Academic Publishers</publisher><pubPlace>Dordrecht</pubPlace><date type="published" when="2002-09-01">2002-09-01</date><biblScope unit="volume">29</biblScope><biblScope unit="issue">3-4</biblScope><biblScope unit="page" from="277">277</biblScope><biblScope unit="page" to="307">307</biblScope></imprint><idno type="ISSN">0168-7433</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0168-7433</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Coq</term><term>formalization of logical systems</term><term>reflection</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: We formalize natural deduction for first-order logic in the proof assistant Coq, using de Bruijn indices for variable binding. The main judgment we model is of the form Γ⊢d [:] φ, stating that d is a proof term of formula φ under hypotheses Γ it can be viewed as a typing relation by the Curry–Howard isomorphism. This relation is proved sound with respect to Coq's native logic and is amenable to the manipulation of formulas and of derivations. As an illustration, we define a reduction relation on proof terms with permutative conversions and prove the property of subject reduction.</div></front></TEI></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000351 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Curation/biblio.hfd -nk 000351 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Istex
|étape= Curation
|type= RBID
|clé= ISTEX:0FB03B36445C9F881F41EAA2510FD268A48850CF
|texte= Proof Reflection in Coq
}}
| This area was generated with Dilib version V0.6.33. |  |