InforLorV4, Hal, Curation, bibRecord, 001512

CoLoR: a Coq library on rewriting and termination

Identifieur interne : 001512 ( Hal/Curation ); précédent : 001511; suivant : 001513

CoLoR: a Coq library on rewriting and termination

Auteurs : Frédéric Blanqui [France] ; Solange Coupet-Grimal [France] ; William Delobel [France] ; Sébastien Hinderer [France] ; Adam Koprowski [Pays-Bas]

Source :

RBID : Hal:inria-00084835

English descriptors

mix :
- Coq, certification, proof, rewriting, termination.

Abstract

Coq is a tool allowing to certify proofs. This paper describes a Coq library for certifying termination proofs.

Url:

https://hal.inria.fr/inria-00084835

Links toward previous steps (curation, corpus...)

to stream Hal, to step Corpus: Pour aller vers cette notice dans l'étape Curation :001512

Links to Exploration step

Hal:inria-00084835

Le document en format XML

<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en">CoLoR: a Coq library on rewriting and termination</title>
<author><name sortKey="Blanqui, Frederic" sort="Blanqui, Frederic" uniqKey="Blanqui F" first="Frédéric" last="Blanqui">Frédéric Blanqui</name>
<affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-2360" status="OLD"><idno type="RNSR">199221357D</idno>
<orgName>Constraints, automatic deduction and software properties proofs</orgName>
<orgName type="acronym">PROTHEO</orgName>
<desc><address><country key="FR"></country>
</address>
<ref type="url">http://www.inria.fr/equipes/protheo</ref>
</desc>
<listRelation><relation active="#struct-160" type="direct"></relation>
<relation name="UMR7503" active="#struct-441569" type="indirect"></relation>
<relation active="#struct-300009" type="indirect"></relation>
<relation active="#struct-300291" type="indirect"></relation>
<relation active="#struct-300292" type="indirect"></relation>
<relation active="#struct-300293" type="indirect"></relation>
<relation active="#struct-2496" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-160" type="direct"><org type="laboratory" xml:id="struct-160" status="OLD"><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName>
<orgName type="acronym">LORIA</orgName>
<desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.loria.fr</ref>
</desc>
<listRelation><relation name="UMR7503" active="#struct-441569" type="direct"></relation>
<relation active="#struct-300009" type="direct"></relation>
<relation active="#struct-300291" type="direct"></relation>
<relation active="#struct-300292" type="direct"></relation>
<relation active="#struct-300293" type="direct"></relation>
</listRelation>
</org>
</tutelle>
<tutelle name="UMR7503" 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-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-300291" type="indirect"><org type="institution" xml:id="struct-300291" status="OLD"><orgName>Université Henri Poincaré - Nancy 1</orgName>
<orgName type="acronym">UHP</orgName>
<date type="end">2011-12-31</date>
<desc><address><addrLine>24-30 rue Lionnois, BP 60120, 54 003 NANCY cedex, France</addrLine>
<country key="FR"></country>
</address>
</desc>
</org>
</tutelle>
<tutelle active="#struct-300292" type="indirect"><org type="institution" xml:id="struct-300292" status="OLD"><orgName>Université Nancy 2</orgName>
<date type="end">2011-12-31</date>
<desc><address><addrLine>91 avenue de la Libération, BP 454, 54001 Nancy cedex</addrLine>
<country key="FR"></country>
</address>
</desc>
</org>
</tutelle>
<tutelle active="#struct-300293" type="indirect"><org type="institution" xml:id="struct-300293" status="OLD"><orgName>Institut National Polytechnique de Lorraine</orgName>
<orgName type="acronym">INPL</orgName>
<date type="end">2011-12-31</date>
<desc><address><country key="FR"></country>
</address>
</desc>
</org>
</tutelle>
<tutelle active="#struct-2496" type="direct"><org type="laboratory" xml:id="struct-2496" status="OLD"><orgName>INRIA Lorraine</orgName>
<desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.inria.fr/centre-de-recherche-inria/nancy-grand-est</ref>
</desc>
<listRelation><relation active="#struct-300009" type="direct"></relation>
</listRelation>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>France</country>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="university">Université Nancy 2</orgName>
<orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="university">Institut national polytechnique de Lorraine</orgName>
<orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName>
</affiliation>
</author>
<author><name sortKey="Coupet Grimal, Solange" sort="Coupet Grimal, Solange" uniqKey="Coupet Grimal S" first="Solange" last="Coupet-Grimal">Solange Coupet-Grimal</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-862" status="OLD"><orgName>Laboratoire d'informatique Fondamentale de Marseille</orgName>
<orgName type="acronym">LIF</orgName>
<desc><address><addrLine>CMI 39, Rue Joliot Curie 13453 MARSEILLE CEDEX 13</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.lif.univ-mrs.fr/</ref>
</desc>
<listRelation><relation active="#struct-5033" type="direct"></relation>
<relation active="#struct-92823" type="direct"></relation>
<relation name="UMR6166" active="#struct-441569" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-5033" type="direct"><org type="institution" xml:id="struct-5033" status="OLD"><idno type="IdRef">026402882</idno>
<orgName>Université de la Méditerranée - Aix-Marseille 2</orgName>
<date type="start">1969</date>
<date type="end">2011</date>
<desc><address><addrLine>58, boulevard Charles Livon - 13284 Marseille cedex 07</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.univmed.fr/</ref>
</desc>
</org>
</tutelle>
<tutelle active="#struct-92823" type="direct"><org type="institution" xml:id="struct-92823" status="OLD"><idno type="IdRef">026403781</idno>
<orgName>Université de Provence - Aix-Marseille 1</orgName>
<date type="end">2011</date>
<desc><address><addrLine>3, place Victor Hugo - 13331 Marseille Cedex 03</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.univ-provence.fr/</ref>
</desc>
</org>
</tutelle>
<tutelle name="UMR6166" 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>
<country>France</country>
</affiliation>
</author>
<author><name sortKey="Delobel, William" sort="Delobel, William" uniqKey="Delobel W" first="William" last="Delobel">William Delobel</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-862" status="OLD"><orgName>Laboratoire d'informatique Fondamentale de Marseille</orgName>
<orgName type="acronym">LIF</orgName>
<desc><address><addrLine>CMI 39, Rue Joliot Curie 13453 MARSEILLE CEDEX 13</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.lif.univ-mrs.fr/</ref>
</desc>
<listRelation><relation active="#struct-5033" type="direct"></relation>
<relation active="#struct-92823" type="direct"></relation>
<relation name="UMR6166" active="#struct-441569" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-5033" type="direct"><org type="institution" xml:id="struct-5033" status="OLD"><idno type="IdRef">026402882</idno>
<orgName>Université de la Méditerranée - Aix-Marseille 2</orgName>
<date type="start">1969</date>
<date type="end">2011</date>
<desc><address><addrLine>58, boulevard Charles Livon - 13284 Marseille cedex 07</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.univmed.fr/</ref>
</desc>
</org>
</tutelle>
<tutelle active="#struct-92823" type="direct"><org type="institution" xml:id="struct-92823" status="OLD"><idno type="IdRef">026403781</idno>
<orgName>Université de Provence - Aix-Marseille 1</orgName>
<date type="end">2011</date>
<desc><address><addrLine>3, place Victor Hugo - 13331 Marseille Cedex 03</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.univ-provence.fr/</ref>
</desc>
</org>
</tutelle>
<tutelle name="UMR6166" 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>
<country>France</country>
</affiliation>
</author>
<author><name sortKey="Hinderer, Sebastien" sort="Hinderer, Sebastien" uniqKey="Hinderer S" first="Sébastien" last="Hinderer">Sébastien Hinderer</name>
<affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-2351" status="OLD"><idno type="RNSR">199421391G</idno>
<orgName>Human-machine dialogue with a significant language component</orgName>
<orgName type="acronym">LANGUE ET DIALOGUE</orgName>
<desc><address><country key="FR"></country>
</address>
</desc>
<listRelation><relation active="#struct-160" type="direct"></relation>
<relation name="UMR7503" active="#struct-441569" type="indirect"></relation>
<relation active="#struct-300009" type="indirect"></relation>
<relation active="#struct-300291" type="indirect"></relation>
<relation active="#struct-300292" type="indirect"></relation>
<relation active="#struct-300293" type="indirect"></relation>
<relation active="#struct-2496" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-160" type="direct"><org type="laboratory" xml:id="struct-160" status="OLD"><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName>
<orgName type="acronym">LORIA</orgName>
<desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.loria.fr</ref>
</desc>
<listRelation><relation name="UMR7503" active="#struct-441569" type="direct"></relation>
<relation active="#struct-300009" type="direct"></relation>
<relation active="#struct-300291" type="direct"></relation>
<relation active="#struct-300292" type="direct"></relation>
<relation active="#struct-300293" type="direct"></relation>
</listRelation>
</org>
</tutelle>
<tutelle name="UMR7503" 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-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-300291" type="indirect"><org type="institution" xml:id="struct-300291" status="OLD"><orgName>Université Henri Poincaré - Nancy 1</orgName>
<orgName type="acronym">UHP</orgName>
<date type="end">2011-12-31</date>
<desc><address><addrLine>24-30 rue Lionnois, BP 60120, 54 003 NANCY cedex, France</addrLine>
<country key="FR"></country>
</address>
</desc>
</org>
</tutelle>
<tutelle active="#struct-300292" type="indirect"><org type="institution" xml:id="struct-300292" status="OLD"><orgName>Université Nancy 2</orgName>
<date type="end">2011-12-31</date>
<desc><address><addrLine>91 avenue de la Libération, BP 454, 54001 Nancy cedex</addrLine>
<country key="FR"></country>
</address>
</desc>
</org>
</tutelle>
<tutelle active="#struct-300293" type="indirect"><org type="institution" xml:id="struct-300293" status="OLD"><orgName>Institut National Polytechnique de Lorraine</orgName>
<orgName type="acronym">INPL</orgName>
<date type="end">2011-12-31</date>
<desc><address><country key="FR"></country>
</address>
</desc>
</org>
</tutelle>
<tutelle active="#struct-2496" type="direct"><org type="laboratory" xml:id="struct-2496" status="OLD"><orgName>INRIA Lorraine</orgName>
<desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.inria.fr/centre-de-recherche-inria/nancy-grand-est</ref>
</desc>
<listRelation><relation active="#struct-300009" type="direct"></relation>
</listRelation>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>France</country>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="university">Université Nancy 2</orgName>
<orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="university">Institut national polytechnique de Lorraine</orgName>
<orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName>
</affiliation>
</author>
<author><name sortKey="Koprowski, Adam" sort="Koprowski, Adam" uniqKey="Koprowski A" first="Adam" last="Koprowski">Adam Koprowski</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-238519" status="VALID"><orgName>Department of mathematics and computing science [Eindhoven]</orgName>
<desc><address><addrLine>P.O. Box 513 5600 MB Eindhoven</addrLine>
<country key="NL"></country>
</address>
<ref type="url">https://www.tue.nl/en/university/departments/mathematics-and-computer-science/</ref>
</desc>
<listRelation><relation active="#struct-4629" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-4629" type="direct"><org type="institution" xml:id="struct-4629" status="VALID"><orgName>Eindhoven University of Technology [Eindhoven]</orgName>
<orgName type="acronym">TUE</orgName>
<desc><address><addrLine>Den Dolech 2 5612 AZ Eindhoven</addrLine>
<country key="NL"></country>
</address>
<ref type="url">http://w3.tue.nl/nl/</ref>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>Pays-Bas</country>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">HAL</idno>
<idno type="RBID">Hal:inria-00084835</idno>
<idno type="halId">inria-00084835</idno>
<idno type="halUri">https://hal.inria.fr/inria-00084835</idno>
<idno type="url">https://hal.inria.fr/inria-00084835</idno>
<date when="2006-08-15">2006-08-15</date>
<idno type="wicri:Area/Hal/Corpus">001512</idno>
<idno type="wicri:Area/Hal/Curation">001512</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en">CoLoR: a Coq library on rewriting and termination</title>
<author><name sortKey="Blanqui, Frederic" sort="Blanqui, Frederic" uniqKey="Blanqui F" first="Frédéric" last="Blanqui">Frédéric Blanqui</name>
<affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-2360" status="OLD"><idno type="RNSR">199221357D</idno>
<orgName>Constraints, automatic deduction and software properties proofs</orgName>
<orgName type="acronym">PROTHEO</orgName>
<desc><address><country key="FR"></country>
</address>
<ref type="url">http://www.inria.fr/equipes/protheo</ref>
</desc>
<listRelation><relation active="#struct-160" type="direct"></relation>
<relation name="UMR7503" active="#struct-441569" type="indirect"></relation>
<relation active="#struct-300009" type="indirect"></relation>
<relation active="#struct-300291" type="indirect"></relation>
<relation active="#struct-300292" type="indirect"></relation>
<relation active="#struct-300293" type="indirect"></relation>
<relation active="#struct-2496" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-160" type="direct"><org type="laboratory" xml:id="struct-160" status="OLD"><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName>
<orgName type="acronym">LORIA</orgName>
<desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.loria.fr</ref>
</desc>
<listRelation><relation name="UMR7503" active="#struct-441569" type="direct"></relation>
<relation active="#struct-300009" type="direct"></relation>
<relation active="#struct-300291" type="direct"></relation>
<relation active="#struct-300292" type="direct"></relation>
<relation active="#struct-300293" type="direct"></relation>
</listRelation>
</org>
</tutelle>
<tutelle name="UMR7503" 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-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-300291" type="indirect"><org type="institution" xml:id="struct-300291" status="OLD"><orgName>Université Henri Poincaré - Nancy 1</orgName>
<orgName type="acronym">UHP</orgName>
<date type="end">2011-12-31</date>
<desc><address><addrLine>24-30 rue Lionnois, BP 60120, 54 003 NANCY cedex, France</addrLine>
<country key="FR"></country>
</address>
</desc>
</org>
</tutelle>
<tutelle active="#struct-300292" type="indirect"><org type="institution" xml:id="struct-300292" status="OLD"><orgName>Université Nancy 2</orgName>
<date type="end">2011-12-31</date>
<desc><address><addrLine>91 avenue de la Libération, BP 454, 54001 Nancy cedex</addrLine>
<country key="FR"></country>
</address>
</desc>
</org>
</tutelle>
<tutelle active="#struct-300293" type="indirect"><org type="institution" xml:id="struct-300293" status="OLD"><orgName>Institut National Polytechnique de Lorraine</orgName>
<orgName type="acronym">INPL</orgName>
<date type="end">2011-12-31</date>
<desc><address><country key="FR"></country>
</address>
</desc>
</org>
</tutelle>
<tutelle active="#struct-2496" type="direct"><org type="laboratory" xml:id="struct-2496" status="OLD"><orgName>INRIA Lorraine</orgName>
<desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.inria.fr/centre-de-recherche-inria/nancy-grand-est</ref>
</desc>
<listRelation><relation active="#struct-300009" type="direct"></relation>
</listRelation>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>France</country>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="university">Université Nancy 2</orgName>
<orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="university">Institut national polytechnique de Lorraine</orgName>
<orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName>
</affiliation>
</author>
<author><name sortKey="Coupet Grimal, Solange" sort="Coupet Grimal, Solange" uniqKey="Coupet Grimal S" first="Solange" last="Coupet-Grimal">Solange Coupet-Grimal</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-862" status="OLD"><orgName>Laboratoire d'informatique Fondamentale de Marseille</orgName>
<orgName type="acronym">LIF</orgName>
<desc><address><addrLine>CMI 39, Rue Joliot Curie 13453 MARSEILLE CEDEX 13</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.lif.univ-mrs.fr/</ref>
</desc>
<listRelation><relation active="#struct-5033" type="direct"></relation>
<relation active="#struct-92823" type="direct"></relation>
<relation name="UMR6166" active="#struct-441569" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-5033" type="direct"><org type="institution" xml:id="struct-5033" status="OLD"><idno type="IdRef">026402882</idno>
<orgName>Université de la Méditerranée - Aix-Marseille 2</orgName>
<date type="start">1969</date>
<date type="end">2011</date>
<desc><address><addrLine>58, boulevard Charles Livon - 13284 Marseille cedex 07</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.univmed.fr/</ref>
</desc>
</org>
</tutelle>
<tutelle active="#struct-92823" type="direct"><org type="institution" xml:id="struct-92823" status="OLD"><idno type="IdRef">026403781</idno>
<orgName>Université de Provence - Aix-Marseille 1</orgName>
<date type="end">2011</date>
<desc><address><addrLine>3, place Victor Hugo - 13331 Marseille Cedex 03</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.univ-provence.fr/</ref>
</desc>
</org>
</tutelle>
<tutelle name="UMR6166" 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>
<country>France</country>
</affiliation>
</author>
<author><name sortKey="Delobel, William" sort="Delobel, William" uniqKey="Delobel W" first="William" last="Delobel">William Delobel</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-862" status="OLD"><orgName>Laboratoire d'informatique Fondamentale de Marseille</orgName>
<orgName type="acronym">LIF</orgName>
<desc><address><addrLine>CMI 39, Rue Joliot Curie 13453 MARSEILLE CEDEX 13</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.lif.univ-mrs.fr/</ref>
</desc>
<listRelation><relation active="#struct-5033" type="direct"></relation>
<relation active="#struct-92823" type="direct"></relation>
<relation name="UMR6166" active="#struct-441569" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-5033" type="direct"><org type="institution" xml:id="struct-5033" status="OLD"><idno type="IdRef">026402882</idno>
<orgName>Université de la Méditerranée - Aix-Marseille 2</orgName>
<date type="start">1969</date>
<date type="end">2011</date>
<desc><address><addrLine>58, boulevard Charles Livon - 13284 Marseille cedex 07</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.univmed.fr/</ref>
</desc>
</org>
</tutelle>
<tutelle active="#struct-92823" type="direct"><org type="institution" xml:id="struct-92823" status="OLD"><idno type="IdRef">026403781</idno>
<orgName>Université de Provence - Aix-Marseille 1</orgName>
<date type="end">2011</date>
<desc><address><addrLine>3, place Victor Hugo - 13331 Marseille Cedex 03</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.univ-provence.fr/</ref>
</desc>
</org>
</tutelle>
<tutelle name="UMR6166" 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>
<country>France</country>
</affiliation>
</author>
<author><name sortKey="Hinderer, Sebastien" sort="Hinderer, Sebastien" uniqKey="Hinderer S" first="Sébastien" last="Hinderer">Sébastien Hinderer</name>
<affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-2351" status="OLD"><idno type="RNSR">199421391G</idno>
<orgName>Human-machine dialogue with a significant language component</orgName>
<orgName type="acronym">LANGUE ET DIALOGUE</orgName>
<desc><address><country key="FR"></country>
</address>
</desc>
<listRelation><relation active="#struct-160" type="direct"></relation>
<relation name="UMR7503" active="#struct-441569" type="indirect"></relation>
<relation active="#struct-300009" type="indirect"></relation>
<relation active="#struct-300291" type="indirect"></relation>
<relation active="#struct-300292" type="indirect"></relation>
<relation active="#struct-300293" type="indirect"></relation>
<relation active="#struct-2496" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-160" type="direct"><org type="laboratory" xml:id="struct-160" status="OLD"><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName>
<orgName type="acronym">LORIA</orgName>
<desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.loria.fr</ref>
</desc>
<listRelation><relation name="UMR7503" active="#struct-441569" type="direct"></relation>
<relation active="#struct-300009" type="direct"></relation>
<relation active="#struct-300291" type="direct"></relation>
<relation active="#struct-300292" type="direct"></relation>
<relation active="#struct-300293" type="direct"></relation>
</listRelation>
</org>
</tutelle>
<tutelle name="UMR7503" 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-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-300291" type="indirect"><org type="institution" xml:id="struct-300291" status="OLD"><orgName>Université Henri Poincaré - Nancy 1</orgName>
<orgName type="acronym">UHP</orgName>
<date type="end">2011-12-31</date>
<desc><address><addrLine>24-30 rue Lionnois, BP 60120, 54 003 NANCY cedex, France</addrLine>
<country key="FR"></country>
</address>
</desc>
</org>
</tutelle>
<tutelle active="#struct-300292" type="indirect"><org type="institution" xml:id="struct-300292" status="OLD"><orgName>Université Nancy 2</orgName>
<date type="end">2011-12-31</date>
<desc><address><addrLine>91 avenue de la Libération, BP 454, 54001 Nancy cedex</addrLine>
<country key="FR"></country>
</address>
</desc>
</org>
</tutelle>
<tutelle active="#struct-300293" type="indirect"><org type="institution" xml:id="struct-300293" status="OLD"><orgName>Institut National Polytechnique de Lorraine</orgName>
<orgName type="acronym">INPL</orgName>
<date type="end">2011-12-31</date>
<desc><address><country key="FR"></country>
</address>
</desc>
</org>
</tutelle>
<tutelle active="#struct-2496" type="direct"><org type="laboratory" xml:id="struct-2496" status="OLD"><orgName>INRIA Lorraine</orgName>
<desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.inria.fr/centre-de-recherche-inria/nancy-grand-est</ref>
</desc>
<listRelation><relation active="#struct-300009" type="direct"></relation>
</listRelation>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>France</country>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="university">Université Nancy 2</orgName>
<orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="university">Institut national polytechnique de Lorraine</orgName>
<orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName>
</affiliation>
</author>
<author><name sortKey="Koprowski, Adam" sort="Koprowski, Adam" uniqKey="Koprowski A" first="Adam" last="Koprowski">Adam Koprowski</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-238519" status="VALID"><orgName>Department of mathematics and computing science [Eindhoven]</orgName>
<desc><address><addrLine>P.O. Box 513 5600 MB Eindhoven</addrLine>
<country key="NL"></country>
</address>
<ref type="url">https://www.tue.nl/en/university/departments/mathematics-and-computer-science/</ref>
</desc>
<listRelation><relation active="#struct-4629" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-4629" type="direct"><org type="institution" xml:id="struct-4629" status="VALID"><orgName>Eindhoven University of Technology [Eindhoven]</orgName>
<orgName type="acronym">TUE</orgName>
<desc><address><addrLine>Den Dolech 2 5612 AZ Eindhoven</addrLine>
<country key="NL"></country>
</address>
<ref type="url">http://w3.tue.nl/nl/</ref>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>Pays-Bas</country>
</affiliation>
</author>
</analytic>
</biblStruct>
</sourceDesc>
</fileDesc>
<profileDesc><textClass><keywords scheme="mix" xml:lang="en"><term>Coq</term>
<term>certification</term>
<term>proof</term>
<term>rewriting</term>
<term>termination</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Coq is a tool allowing to certify proofs. This paper describes a Coq library for certifying termination proofs.</div>
</front>
</TEI>
<hal api="V3"><titleStmt><title xml:lang="en">CoLoR: a Coq library on rewriting and termination</title>
<author role="aut"><persName><forename type="first">Frédéric</forename>
<surname>Blanqui</surname>
</persName>
<email>blanqui@loria.fr</email>
<idno type="halauthor">58558</idno>
<orgName ref="#struct-300009"></orgName>
<affiliation ref="#struct-2360"></affiliation>
</author>
<author role="aut"><persName><forename type="first">Solange</forename>
<surname>Coupet-Grimal</surname>
</persName>
<email>Solange.Coupet@cmi.univ-mrs.fr</email>
<idno type="halauthor">111726</idno>
<orgName ref="#struct-364328"></orgName>
<affiliation ref="#struct-862"></affiliation>
</author>
<author role="aut"><persName><forename type="first">William</forename>
<surname>Delobel</surname>
</persName>
<email>delobel@cmi.univ-mrs.fr</email>
<idno type="halauthor">111727</idno>
<orgName ref="#struct-364328"></orgName>
<affiliation ref="#struct-862"></affiliation>
</author>
<author role="aut"><persName><forename type="first">Sébastien</forename>
<surname>Hinderer</surname>
</persName>
<email>Sebastien.Hinderer@loria.fr</email>
<idno type="halauthor">111728</idno>
<orgName ref="#struct-300291"></orgName>
<affiliation ref="#struct-2351"></affiliation>
</author>
<author role="aut"><persName><forename type="first">Adam</forename>
<surname>Koprowski</surname>
</persName>
<email>A.Koprowski@tue.nl</email>
<idno type="halauthor">111729</idno>
<orgName ref="#struct-4629"></orgName>
<affiliation ref="#struct-238519"></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"><date type="whenSubmitted">2006-08-31 16:46:49</date>
</edition>
<edition n="v2" type="current"><date type="whenSubmitted">2006-09-11 13:48:39</date>
<date type="whenWritten">2005</date>
<date type="whenModified">2016-05-19 01:09:26</date>
<date type="whenReleased">2006-09-11 13:59:11</date>
<date type="whenProduced">2006-08-15</date>
<date type="whenEndEmbargoed">2006-09-11</date>
<ref type="file" target="https://hal.inria.fr/inria-00084835v2/document"><date notBefore="2006-09-11"></date>
</ref>
<ref type="file" n="1" target="https://hal.inria.fr/inria-00084835/file/main.pdf"><date notBefore="2006-09-11"></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-00084835</idno>
<idno type="halUri">https://hal.inria.fr/inria-00084835</idno>
<idno type="halBibtex">blanqui:inria-00084835</idno>
<idno type="halRefHtml">Eighth International Workshop on Termination - WST 2006, Aug 2006, Seattle, United States. 2006</idno>
<idno type="halRef">Eighth International Workshop on Termination - WST 2006, Aug 2006, Seattle, United States. 2006</idno>
</publicationStmt>
<seriesStmt><idno type="stamp" n="INRIA">INRIA - Institut National de Recherche en Informatique et en Automatique</idno>
<idno type="stamp" n="CNRS">CNRS - Centre national de la recherche scientifique</idno>
<idno type="stamp" n="INPL">Institut National Polytechnique de Lorraine</idno>
<idno type="stamp" n="LIF">Laboratoire d'informatique fondamentale de Marseille</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">LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications</idno>
<idno type="stamp" n="LORIA-FM" p="LORIA">Méthodes formelles</idno>
<idno type="stamp" n="UNIV-AMU">Aix Marseille Université</idno>
<idno type="stamp" n="UNIV-LORRAINE">Université de Lorraine</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>
</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">CoLoR: a Coq library on rewriting and termination</title>
<author role="aut"><persName><forename type="first">Frédéric</forename>
<surname>Blanqui</surname>
</persName>
<email>blanqui@loria.fr</email>
<idno type="halAuthorId">58558</idno>
<orgName ref="#struct-300009"></orgName>
<affiliation ref="#struct-2360"></affiliation>
</author>
<author role="aut"><persName><forename type="first">Solange</forename>
<surname>Coupet-Grimal</surname>
</persName>
<email>Solange.Coupet@cmi.univ-mrs.fr</email>
<idno type="halAuthorId">111726</idno>
<orgName ref="#struct-364328"></orgName>
<affiliation ref="#struct-862"></affiliation>
</author>
<author role="aut"><persName><forename type="first">William</forename>
<surname>Delobel</surname>
</persName>
<email>delobel@cmi.univ-mrs.fr</email>
<idno type="halAuthorId">111727</idno>
<orgName ref="#struct-364328"></orgName>
<affiliation ref="#struct-862"></affiliation>
</author>
<author role="aut"><persName><forename type="first">Sébastien</forename>
<surname>Hinderer</surname>
</persName>
<email>Sebastien.Hinderer@loria.fr</email>
<idno type="halAuthorId">111728</idno>
<orgName ref="#struct-300291"></orgName>
<affiliation ref="#struct-2351"></affiliation>
</author>
<author role="aut"><persName><forename type="first">Adam</forename>
<surname>Koprowski</surname>
</persName>
<email>A.Koprowski@tue.nl</email>
<idno type="halAuthorId">111729</idno>
<orgName ref="#struct-4629"></orgName>
<affiliation ref="#struct-238519"></affiliation>
</author>
</analytic>
<monogr><meeting><title>Eighth International Workshop on Termination - WST 2006</title>
<date type="start">2006-08-15</date>
<settlement>Seattle</settlement>
<country key="US">United States</country>
</meeting>
<imprint><date type="datePub">2006</date>
</imprint>
</monogr>
</biblStruct>
</sourceDesc>
<profileDesc><langUsage><language ident="en">English</language>
</langUsage>
<textClass><keywords scheme="author"><term xml:lang="en">Coq</term>
<term xml:lang="en">proof</term>
<term xml:lang="en">termination</term>
<term xml:lang="en">certification</term>
<term xml:lang="en">rewriting</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">Coq is a tool allowing to certify proofs. This paper describes a Coq library for certifying termination proofs.</abstract>
</profileDesc>
</hal>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Hal/Curation

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001512 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Hal/Curation/biblio.hfd -nk 001512 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Hal
   |étape=   Curation
   |type=    RBID
   |clé=     Hal:inria-00084835
   |texte=   CoLoR: a Coq library on rewriting and termination
}}

This area was generated with Dilib version V0.6.33.
Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022

	Serveur d'exploration sur la recherche en informatique en Lorraine
	Attention, ce site est en cours de développement ! Attention, site généré par des moyens informatiques à partir de corpus bruts. Les informations ne sont donc pas validées.

Serveur d'exploration sur la recherche en informatique en Lorraine

CoLoR: a Coq library on rewriting and termination

CoLoR: a Coq library on rewriting and termination

Source :

English descriptors

Abstract

Links toward previous steps (curation, corpus...)

Links to Exploration step

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri