A Lambda-Free Higher-Order Recursive Path Order

Abstract : We generalize the recursive path order (RPO) to higher-order terms without λ-abstraction. This new order fully coincides with the standard RPO on first-order terms also in the presence of currying, distinguishing it from previous work. It has many useful properties, including well-foundedness, transitivity, stability under substitution, and the subterm property. It appears promising as the basis of a higher-order superposition calculus.
Type de document :
Communication dans un congrès
Javier Esparza and Andrzej S. Murawski. Foundations of Software Science and Computation Structures, 20th International Conference (FOSSACS 2017), Apr 2017, Uppsala, Sweden. Springer, 10203, pp.461-479, 2017, Lecture Notes in Computer Science. 〈10.1007/978-3-662-54458-7_27〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01592189
Contributeur : Stephan Merz <>
Soumis le : mercredi 27 septembre 2017 - 18:44:57
Dernière modification le : samedi 30 septembre 2017 - 01:20:58

Fichier

BlanchetteWaldmannWandFoSSaCS....
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Jasmin Blanchette, Uwe Waldmann, Daniel Wand. A Lambda-Free Higher-Order Recursive Path Order. Javier Esparza and Andrzej S. Murawski. Foundations of Software Science and Computation Structures, 20th International Conference (FOSSACS 2017), Apr 2017, Uppsala, Sweden. Springer, 10203, pp.461-479, 2017, Lecture Notes in Computer Science. 〈10.1007/978-3-662-54458-7_27〉. 〈hal-01592189〉

Partager

Métriques

Consultations de
la notice

46

Téléchargements du document

4