Normal Higher-Order Termination

Abstract : We extend the termination proof methods based on reduction orderings to higher-order rewriting systems based on higher-order pattern matching. We accommodate, on the one hand, a weakly polymorphic, algebraic extension of Church's simply typed λ-calculus, and on the other hand, any use of eta, as a reduction, as an expansion or as an equation. The user's rules may be of any type in this type system, either a base, functional, or weakly polymorphic type.
Type de document :
Article dans une revue
ACM Transactions on Computational Logic, Association for Computing Machinery, 2013, 〈10.1145/26999.13〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01239068
Contributeur : Jean-Pierre Jouannaud <>
Soumis le : lundi 7 décembre 2015 - 13:32:39
Dernière modification le : jeudi 10 mai 2018 - 02:07:00
Document(s) archivé(s) le : samedi 29 avril 2017 - 09:35:59

Fichier

acmsubmission-final.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Jean-Pierre Jouannaud, Albert Rubio. Normal Higher-Order Termination. ACM Transactions on Computational Logic, Association for Computing Machinery, 2013, 〈10.1145/26999.13〉. 〈hal-01239068〉

Partager

Métriques

Consultations de la notice

193

Téléchargements de fichiers

45