Size-based termination of higher-order rewriting

Abstract : We provide a general and modular criterion for the termination of simply-typed λ -calculus extended with function symbols defined by user-defined rewrite rules. Following a work of Hughes, Pareto and Sabry for functions defined with a fixpoint operator and pattern-matching, several criteria use typing rules for bounding the height of arguments in function calls. In this paper, we extend this approach to rewriting-based function definitions and more general user-defined notions of size.
Type de document :
Article dans une revue
Journal of Functional Programming, Cambridge University Press (CUP), 2018, 〈10.1017/S0956796818000072〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01424921
Contributeur : Frédéric Blanqui <>
Soumis le : mardi 20 février 2018 - 12:42:22
Dernière modification le : lundi 23 avril 2018 - 16:40:03

Fichiers

Identifiants

Citation

Frédéric Blanqui. Size-based termination of higher-order rewriting. Journal of Functional Programming, Cambridge University Press (CUP), 2018, 〈10.1017/S0956796818000072〉. 〈hal-01424921v5〉

Partager

Métriques

Consultations de la notice

111

Téléchargements de fichiers

46