Higher-order dependency pairs

Frédéric Blanqui 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Arts and Giesl proved that the termination of a first-order rewrite system can be reduced to the study of its ``dependency pairs''. We extend these results to rewrite systems on simply typed lambda-terms by using Tait's computability technique.
Type de document :
Communication dans un congrès
Eighth International Workshop on Termination - WST 2006, Aug 2006, Seattle, United States. 2006
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00084821
Contributeur : Frédéric Blanqui <>
Soumis le : lundi 11 septembre 2006 - 13:45:15
Dernière modification le : mercredi 25 avril 2018 - 01:33:00
Document(s) archivé(s) le : lundi 20 septembre 2010 - 16:55:47

Fichiers

Identifiants

  • HAL Id : inria-00084821, version 2

Collections

Citation

Frédéric Blanqui. Higher-order dependency pairs. Eighth International Workshop on Termination - WST 2006, Aug 2006, Seattle, United States. 2006. 〈inria-00084821v2〉

Partager

Métriques

Consultations de la notice

133

Téléchargements de fichiers

61