HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

The computability path ordering: the end of a quest

Frédéric Blanqui 1, 2 Jean-Pierre Jouannaud 3, 4 Albert Rubio 5
1 FORMES - Formal Methods for Embedded Systems
LIAMA - Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées, Inria Paris-Rocquencourt
2 PAREO - Formal islands: foundations and applications
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
4 TYPICAL - Types, Logic and computing
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
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.
Document type :
Conference papers
Complete list of metadata

Cited literature [50 references]  Display  Hide  Download

Contributor : Frédéric Blanqui Connect in order to contact the contributor
Submitted on : Monday, June 16, 2008 - 12:07:28 PM
Last modification on : Friday, January 21, 2022 - 3:16:02 AM
Long-term archiving on: : Tuesday, September 21, 2010 - 5:00:53 PM


Files produced by the author(s)


  • HAL Id : inria-00288209, version 2
  • ARXIV : 0806.2517



Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio. The computability path ordering: the end of a quest. 7th EACSL Annual Conference on Computer Science Logic - CSL'08, Sep 2008, Bertinoro, Italy. ⟨inria-00288209v2⟩



Record views


Files downloads