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, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR
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.
Type de document :
Communication dans un congrès
7th EACSL Annual Conference on Computer Science Logic - CSL'08, Sep 2008, Bertinoro, Italy. 5213, 2008, LNCS
Liste complète des métadonnées

Littérature citée [50 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00288209
Contributeur : Frédéric Blanqui <>
Soumis le : lundi 16 juin 2008 - 12:07:28
Dernière modification le : jeudi 11 janvier 2018 - 06:22:29
Document(s) archivé(s) le : mardi 21 septembre 2010 - 17:00:53

Fichiers

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

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

Collections

Citation

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. 5213, 2008, LNCS. 〈inria-00288209v2〉

Partager

Métriques

Consultations de la notice

429

Téléchargements de fichiers

234