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 <>
Submitted on : Monday, June 16, 2008 - 12:07:28 PM
Last modification on : Friday, February 26, 2021 - 3:28:08 PM
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