InforLorV4, Hal, Corpus, bibRecord, 004C33

The computability path ordering: the end of a quest

Identifieur interne : 004C33 ( Hal/Corpus ); précédent : 004C32; suivant : 004C34

The computability path ordering: the end of a quest

Auteurs : Frédéric Blanqui ; Jean-Pierre Jouannaud ; Albert Rubio

Source :

RBID : Hal:inria-00288209

English descriptors

mix :
- lambda-calculus, rewriting, term ordering, termination.

Abstract

In this paper, we first briefly survey automated termination proof methods for higher-order calculi. We then concentrate on the higher-order recursive path ordering, for which we provide an improved definition, the Computability Path Ordering. This new definition appears indeed to capture the essence of computability arguments à la Tait and Girard, therefore explaining the name of the improved ordering.

Url:

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

Links to Exploration step

Hal:inria-00288209

Le document en format XML

<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en">The computability path ordering: the end of a quest</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="Rubio, Albert" sort="Rubio, Albert" uniqKey="Rubio A" first="Albert" last="Rubio">Albert Rubio</name>
<affiliation><hal:affiliation type="laboratory" xml:id="struct-74848" status="VALID"><orgName>Llenguatges i Sistemes Informàtics</orgName>
<orgName type="acronym">LSI</orgName>
<desc><address><addrLine>Universitat Politécnica de Catalunya FIB / FME C/ Pau Gargallo 5, E-Barcelona 08028</addrLine>
<country key="ES"></country>
</address>
<ref type="url">http://www.lsi.upc.edu/</ref>
</desc>
<listRelation><relation active="#struct-85878" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-85878" type="direct"><org type="institution" xml:id="struct-85878" status="VALID"><orgName>Universitat Politècnica de Catalunya [Barcelona]</orgName>
<orgName type="acronym">UPC</orgName>
<desc><address><addrLine>Universitat Politècnica de Catalunya C. Jordi Girona, 31. 08034 Barcelona</addrLine>
<country key="ES"></country>
</address>
<ref type="url">http://www.upc.edu/</ref>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">HAL</idno>
<idno type="RBID">Hal:inria-00288209</idno>
<idno type="halId">inria-00288209</idno>
<idno type="halUri">https://hal.inria.fr/inria-00288209</idno>
<idno type="url">https://hal.inria.fr/inria-00288209</idno>
<date when="2008-09-15">2008-09-15</date>
<idno type="wicri:Area/Hal/Corpus">004C33</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en">The computability path ordering: the end of a quest</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="Rubio, Albert" sort="Rubio, Albert" uniqKey="Rubio A" first="Albert" last="Rubio">Albert Rubio</name>
<affiliation><hal:affiliation type="laboratory" xml:id="struct-74848" status="VALID"><orgName>Llenguatges i Sistemes Informàtics</orgName>
<orgName type="acronym">LSI</orgName>
<desc><address><addrLine>Universitat Politécnica de Catalunya FIB / FME C/ Pau Gargallo 5, E-Barcelona 08028</addrLine>
<country key="ES"></country>
</address>
<ref type="url">http://www.lsi.upc.edu/</ref>
</desc>
<listRelation><relation active="#struct-85878" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-85878" type="direct"><org type="institution" xml:id="struct-85878" status="VALID"><orgName>Universitat Politècnica de Catalunya [Barcelona]</orgName>
<orgName type="acronym">UPC</orgName>
<desc><address><addrLine>Universitat Politècnica de Catalunya C. Jordi Girona, 31. 08034 Barcelona</addrLine>
<country key="ES"></country>
</address>
<ref type="url">http://www.upc.edu/</ref>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
</affiliation>
</author>
</analytic>
</biblStruct>
</sourceDesc>
</fileDesc>
<profileDesc><textClass><keywords scheme="mix" xml:lang="en"><term>lambda-calculus</term>
<term>rewriting</term>
<term>term ordering</term>
<term>termination</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">In this paper, we first briefly survey automated termination proof methods for higher-order calculi. We then concentrate on the higher-order recursive path ordering, for which we provide an improved definition, the Computability Path Ordering. This new definition appears indeed to capture the essence of computability arguments à la Tait and Girard, therefore explaining the name of the improved ordering.</div>
</front>
</TEI>
<hal api="V3"><titleStmt><title xml:lang="en">The computability path ordering: the end of a quest</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">Albert</forename>
<surname>Rubio</surname>
</persName>
<email>rubio@lsi.upc.edu</email>
<idno type="halauthor">120660</idno>
<orgName ref="#struct-85878"></orgName>
<affiliation ref="#struct-74848"></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">2008-06-16 09:53:09</date>
</edition>
<edition n="v2" type="current"><date type="whenSubmitted">2008-06-16 12:07:28</date>
<date type="whenModified">2016-05-18 09:01:08</date>
<date type="whenReleased">2008-06-16 13:39:32</date>
<date type="whenProduced">2008-09-15</date>
<date type="whenEndEmbargoed">2008-06-16</date>
<ref type="file" target="https://hal.inria.fr/inria-00288209v2/document"><date notBefore="2008-06-16"></date>
</ref>
<ref type="file" subtype="author" n="1" target="https://hal.inria.fr/inria-00288209/file/main.pdf"><date notBefore="2008-06-16"></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-00288209</idno>
<idno type="halUri">https://hal.inria.fr/inria-00288209</idno>
<idno type="halBibtex">blanqui:inria-00288209</idno>
<idno type="halRefHtml">7th EACSL Annual Conference on Computer Science Logic - CSL'08, Sep 2008, Bertinoro, Italy. 5213, 2008, LNCS</idno>
<idno type="halRef">7th EACSL Annual Conference on Computer Science Logic - CSL'08, Sep 2008, Bertinoro, Italy. 5213, 2008, LNCS</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">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="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="1">Yes</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">The computability path ordering: the end of a quest</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">Albert</forename>
<surname>Rubio</surname>
</persName>
<email>rubio@lsi.upc.edu</email>
<idno type="halAuthorId">120660</idno>
<orgName ref="#struct-85878"></orgName>
<affiliation ref="#struct-74848"></affiliation>
</author>
</analytic>
<monogr><meeting><title>7th EACSL Annual Conference on Computer Science Logic - CSL'08</title>
<date type="start">2008-09-15</date>
<settlement>Bertinoro</settlement>
<country key="IT">Italy</country>
</meeting>
<imprint><biblScope unit="serie">LNCS</biblScope>
<biblScope unit="volume">5213</biblScope>
<date type="datePub">2008</date>
</imprint>
</monogr>
<idno type="arxiv">0806.2517</idno>
</biblStruct>
</sourceDesc>
<profileDesc><langUsage><language ident="en">English</language>
</langUsage>
<textClass><keywords scheme="author"><term xml:lang="en">termination</term>
<term xml:lang="en">rewriting</term>
<term xml:lang="en">term ordering</term>
<term xml:lang="en">lambda-calculus</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">In this paper, we first briefly survey automated termination proof methods for higher-order calculi. We then concentrate on the higher-order recursive path ordering, for which we provide an improved definition, the Computability Path Ordering. This new definition appears indeed to capture the essence of computability arguments à la Tait and Girard, therefore explaining the name of the improved ordering.</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 004C33 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Hal/Corpus/biblio.hfd -nk 004C33 | 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-00288209
   |texte=   The computability path ordering: the end of a quest
}}

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

The computability path ordering: the end of a quest

The computability path ordering: the end of a quest

Source :

English descriptors

Abstract

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