Proof Reflection in Coq
Identifieur interne : 000353 ( Istex/Corpus ); précédent : 000352; suivant : 000354Proof 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 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></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><istex><corpusName>springer-journals</corpusName><author><json:item><name>Dimitri Hendriks</name></json:item></author><subject><json:item><lang><json:string>eng</json:string></lang><value>Coq</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>formalization of logical systems</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>reflection</value></json:item></subject><articleId><json:string>5109768</json:string><json:string>Art5</json:string></articleId><arkIstex>ark:/67375/VQC-R56L80GL-1</arkIstex><language><json:string>eng</json:string></language><originalGenre><json:string>OriginalPaper</json:string></originalGenre><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.</abstract><qualityIndicators><score>8.176</score><pdfWordCount>11207</pdfWordCount><pdfCharCount>49182</pdfCharCount><pdfVersion>1.3</pdfVersion><pdfPageCount>31</pdfPageCount><pdfPageSize>595 x 842 pts (A4)</pdfPageSize><refBibsNative>false</refBibsNative><abstractWordCount>98</abstractWordCount><abstractCharCount>596</abstractCharCount><keywordCount>3</keywordCount></qualityIndicators><title>Proof Reflection in Coq</title><genre><json:string>research-article</json:string></genre><host><title>Journal of Automated Reasoning</title><language><json:string>unknown</json:string></language><publicationDate>2002</publicationDate><copyrightDate>2002</copyrightDate><issn><json:string>0168-7433</json:string></issn><eissn><json:string>1573-0670</json:string></eissn><journalId><json:string>10817</json:string></journalId><volume>29</volume><issue>3-4</issue><pages><first>277</first><last>307</last></pages><genre><json:string>journal</json:string></genre><subject><json:item><value>Logic</value></json:item><json:item><value>Symbolic and Algebraic Manipulation</value></json:item><json:item><value>Artificial Intelligence (incl. Robotics)</value></json:item><json:item><value>Mathematical Logic and Foundations</value></json:item></subject></host><ark><json:string>ark:/67375/VQC-R56L80GL-1</json:string></ark><publicationDate>2002</publicationDate><copyrightDate>2002</copyrightDate><doi><json:string>10.1023/A:1021923116629</json:string></doi><id>0FB03B36445C9F881F41EAA2510FD268A48850CF</id><score>1</score><fulltext><json:item><extension>pdf</extension><original>true</original><mimetype>application/pdf</mimetype><uri>https://api.istex.fr/ark:/67375/VQC-R56L80GL-1/fulltext.pdf</uri></json:item><json:item><extension>zip</extension><original>false</original><mimetype>application/zip</mimetype><uri>https://api.istex.fr/ark:/67375/VQC-R56L80GL-1/bundle.zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/ark:/67375/VQC-R56L80GL-1/fulltext.tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Proof Reflection in Coq</title></titleStmt><publicationStmt><authority>ISTEX</authority><publisher scheme="https://scientific-publisher.data.istex.fr">Kluwer Academic Publishers</publisher><pubPlace>Dordrecht</pubPlace><availability><licence><p>Kluwer Academic Publishers, 2002</p></licence><p scheme="https://loaded-corpus.data.istex.fr/ark:/67375/XBH-3XSW68JL-F">springer</p></availability><date>2002</date></publicationStmt><notesStmt><note type="research-article" scheme="https://content-type.data.istex.fr/ark:/67375/XTP-1JC4F85T-7">research-article</note><note type="journal" scheme="https://publication-type.data.istex.fr/ark:/67375/JMC-0GLKJH51-B">journal</note></notesStmt><sourceDesc><biblStruct type="inbook"><analytic><title level="a" type="main" xml:lang="en">Proof Reflection in Coq</title><author xml:id="author-0000"><persName><forename type="first">Dimitri</forename><surname>Hendriks</surname></persName></author><idno type="istex">0FB03B36445C9F881F41EAA2510FD268A48850CF</idno><idno type="ark">ark:/67375/VQC-R56L80GL-1</idno><idno type="DOI">10.1023/A:1021923116629</idno><idno type="article-id">5109768</idno><idno type="article-id">Art5</idno></analytic><monogr><title level="j">Journal of Automated Reasoning</title><title level="j" type="abbrev">Journal of Automated Reasoning</title><idno type="pISSN">0168-7433</idno><idno type="eISSN">1573-0670</idno><idno type="journal-ID">true</idno><idno type="issue-article-count">12</idno><idno type="volume-issue-count">4</idno><imprint><publisher>Kluwer Academic Publishers</publisher><pubPlace>Dordrecht</pubPlace><date type="published" when="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></monogr></biblStruct></sourceDesc></fileDesc><profileDesc><creation><date>2002</date></creation><langUsage><language ident="en">en</language></langUsage><abstract xml:lang="en"><p>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.</p></abstract><textClass xml:lang="en"><keywords scheme="keyword"><list><item><term>Coq</term></item><item><term>formalization of logical systems</term></item><item><term>reflection</term></item></list></keywords></textClass><textClass><keywords scheme="Journal Subject"><list><head>Philosophy</head><item><term>Logic</term></item><item><term>Symbolic and Algebraic Manipulation</term></item><item><term>Artificial Intelligence (incl. Robotics)</term></item><item><term>Mathematical Logic and Foundations</term></item></list></keywords></textClass></profileDesc><revisionDesc><change when="2002-09-01">Published</change></revisionDesc></teiHeader></istex:fulltextTEI><json:item><extension>txt</extension><original>false</original><mimetype>text/plain</mimetype><uri>https://api.istex.fr/ark:/67375/VQC-R56L80GL-1/fulltext.txt</uri></json:item></fulltext><metadata><istex:metadataXml wicri:clean="corpus springer-journals not found" wicri:toSee="no header"><istex:xmlDeclaration>version="1.0" encoding="UTF-8"</istex:xmlDeclaration><istex:docType PUBLIC="-//Springer-Verlag//DTD A++ V2.4//EN" URI="http://devel.springer.de/A++/V2.4/DTD/A++V2.4.dtd" name="istex:docType"></istex:docType><istex:document><Publisher><PublisherInfo><PublisherName>Kluwer Academic Publishers</PublisherName><PublisherLocation>Dordrecht</PublisherLocation></PublisherInfo><Journal><JournalInfo JournalProductType="ArchiveJournal" NumberingStyle="Unnumbered"><JournalID>10817</JournalID><JournalPrintISSN>0168-7433</JournalPrintISSN><JournalElectronicISSN>1573-0670</JournalElectronicISSN><JournalTitle>Journal of Automated Reasoning</JournalTitle><JournalAbbreviatedTitle>Journal of Automated Reasoning</JournalAbbreviatedTitle><JournalSubjectGroup><JournalSubject Type="Primary">Philosophy</JournalSubject><JournalSubject Type="Secondary">Logic</JournalSubject><JournalSubject Type="Secondary">Symbolic and Algebraic Manipulation</JournalSubject><JournalSubject Type="Secondary">Artificial Intelligence (incl. Robotics)</JournalSubject><JournalSubject Type="Secondary">Mathematical Logic and Foundations</JournalSubject></JournalSubjectGroup></JournalInfo><Volume><VolumeInfo VolumeType="Regular" TocLevels="0"><VolumeIDStart>29</VolumeIDStart><VolumeIDEnd>29</VolumeIDEnd><VolumeIssueCount>4</VolumeIssueCount></VolumeInfo><Issue IssueType="Combined"><IssueInfo TocLevels="0"><IssueIDStart>3</IssueIDStart><IssueIDEnd>4</IssueIDEnd><IssueArticleCount>12</IssueArticleCount><IssueHistory><CoverDate><DateString>2002</DateString><Year>2002</Year><Month>9</Month></CoverDate></IssueHistory><IssueCopyright><CopyrightHolderName>Kluwer Academic Publishers</CopyrightHolderName><CopyrightYear>2002</CopyrightYear></IssueCopyright></IssueInfo><Article ID="Art5"><ArticleInfo Language="En" ArticleType="OriginalPaper" NumberingStyle="Unnumbered" TocLevels="0" ContainsESM="No"><ArticleID>5109768</ArticleID><ArticleDOI>10.1023/A:1021923116629</ArticleDOI><ArticleSequenceNumber>5</ArticleSequenceNumber><ArticleTitle Language="En">Proof Reflection in Coq</ArticleTitle><ArticleFirstPage>277</ArticleFirstPage><ArticleLastPage>307</ArticleLastPage><ArticleHistory><RegistrationDate><Year>2004</Year><Month>9</Month><Day>30</Day></RegistrationDate></ArticleHistory><ArticleCopyright><CopyrightHolderName>Kluwer Academic Publishers</CopyrightHolderName><CopyrightYear>2002</CopyrightYear></ArticleCopyright><ArticleGrants Type="Regular"><MetadataGrant Grant="OpenAccess"></MetadataGrant><AbstractGrant Grant="OpenAccess"></AbstractGrant><BodyPDFGrant Grant="Restricted"></BodyPDFGrant><BodyHTMLGrant Grant="Restricted"></BodyHTMLGrant><BibliographyGrant Grant="Restricted"></BibliographyGrant><ESMGrant Grant="Restricted"></ESMGrant></ArticleGrants><ArticleContext><JournalID>10817</JournalID><VolumeIDStart>29</VolumeIDStart><VolumeIDEnd>29</VolumeIDEnd><IssueIDStart>3</IssueIDStart><IssueIDEnd>4</IssueIDEnd></ArticleContext></ArticleInfo><ArticleHeader><AuthorGroup><Author><AuthorName DisplayOrder="Western"><GivenName>Dimitri</GivenName><FamilyName>Hendriks</FamilyName></AuthorName></Author></AuthorGroup><Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading><Para>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 Γ⊢<Emphasis Type="Italic">d</Emphasis> [:] φ, stating that <Emphasis Type="Italic">d</Emphasis> 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.</Para></Abstract><KeywordGroup Language="En"><Keyword>Coq</Keyword><Keyword>formalization of logical systems</Keyword><Keyword>reflection</Keyword></KeywordGroup></ArticleHeader><NoBody></NoBody></Article></Issue></Volume></Journal></Publisher></istex:document></istex:metadataXml><mods version="3.6"><titleInfo lang="en"><title>Proof Reflection in Coq</title></titleInfo><titleInfo type="alternative" contentType="CDATA"><title>Proof Reflection in Coq</title></titleInfo><name type="personal"><namePart type="given">Dimitri</namePart><namePart type="family">Hendriks</namePart><role><roleTerm type="text">author</roleTerm></role></name><typeOfResource>text</typeOfResource><genre type="research-article" displayLabel="OriginalPaper" authority="ISTEX" authorityURI="https://content-type.data.istex.fr" valueURI="https://content-type.data.istex.fr/ark:/67375/XTP-1JC4F85T-7">research-article</genre><originInfo><publisher>Kluwer Academic Publishers</publisher><place><placeTerm type="text">Dordrecht</placeTerm></place><dateIssued encoding="w3cdtf">2002-09-01</dateIssued><copyrightDate encoding="w3cdtf">2002</copyrightDate></originInfo><language><languageTerm type="code" authority="rfc3066">en</languageTerm><languageTerm type="code" authority="iso639-2b">eng</languageTerm></language><abstract 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.</abstract><subject lang="en"><topic>Coq</topic><topic>formalization of logical systems</topic><topic>reflection</topic></subject><relatedItem type="host"><titleInfo><title>Journal of Automated Reasoning</title></titleInfo><titleInfo type="abbreviated"><title>Journal of Automated Reasoning</title></titleInfo><genre type="journal" authority="ISTEX" authorityURI="https://publication-type.data.istex.fr" valueURI="https://publication-type.data.istex.fr/ark:/67375/JMC-0GLKJH51-B">journal</genre><originInfo><publisher>Springer</publisher><dateIssued encoding="w3cdtf">2002-09-01</dateIssued><copyrightDate encoding="w3cdtf">2002</copyrightDate></originInfo><subject><genre>Philosophy</genre><topic>Logic</topic><topic>Symbolic and Algebraic Manipulation</topic><topic>Artificial Intelligence (incl. Robotics)</topic><topic>Mathematical Logic and Foundations</topic></subject><identifier type="ISSN">0168-7433</identifier><identifier type="eISSN">1573-0670</identifier><identifier type="JournalID">10817</identifier><identifier type="IssueArticleCount">12</identifier><identifier type="VolumeIssueCount">4</identifier><part><date>2002</date><detail type="volume"><number>29</number><caption>vol.</caption></detail><detail type="issue"><number>3-4</number><caption>no.</caption></detail><extent unit="pages"><start>277</start><end>307</end></extent></part><recordInfo><recordOrigin>Kluwer Academic Publishers, 2002</recordOrigin></recordInfo></relatedItem><identifier type="istex">0FB03B36445C9F881F41EAA2510FD268A48850CF</identifier><identifier type="ark">ark:/67375/VQC-R56L80GL-1</identifier><identifier type="DOI">10.1023/A:1021923116629</identifier><identifier type="ArticleID">5109768</identifier><identifier type="ArticleID">Art5</identifier><accessCondition type="use and reproduction" contentType="copyright">Kluwer Academic Publishers, 2002</accessCondition><recordInfo><recordContentSource authority="ISTEX" authorityURI="https://loaded-corpus.data.istex.fr" valueURI="https://loaded-corpus.data.istex.fr/ark:/67375/XBH-3XSW68JL-F">springer</recordContentSource><recordOrigin>Kluwer Academic Publishers, 2002</recordOrigin></recordInfo></mods><json:item><extension>json</extension><original>false</original><mimetype>application/json</mimetype><uri>https://api.istex.fr/ark:/67375/VQC-R56L80GL-1/record.json</uri></json:item></metadata><serie></serie></istex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000353 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 000353 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Istex
|étape= Corpus
|type= RBID
|clé= ISTEX:0FB03B36445C9F881F41EAA2510FD268A48850CF
|texte= Proof Reflection in Coq
}}
| This area was generated with Dilib version V0.6.33. |  |