Title
HORPO with computability closure: a reconstruction
Abstract
This paper provides a new, decidable definition of the higherorder recursive path ordering in which type comparisons are made only when needed, therefore eliminating the need for the computability closure, and bound variables are handled explicitly, making it possible to handle recursors for arbitrary strictly positive inductive types.
Year
DOI
Venue
2007
10.1007/978-3-540-75560-9_12
international conference on logic programming
Keywords
DocType
Volume
type comparison,higherorder recursive path,computability closure,positive inductive type,bound variable,decidable definition
Conference
abs/0708.3582
ISSN
ISBN
Citations 
Dans 14th International Conference on Logic for Programming Artificial Intelligence and Reasoning LNCS (2007)
3-540-75558-6
7
PageRank 
References 
Authors
0.47
8
3
Name
Order
Citations
PageRank
Frédéric Blanqui129017.96
Jean-Pierre Jouannaud21921227.43
Albert Rubio322819.44