Sciweavers

LPAR
2007
Springer

HORPO with Computability Closure: A Reconstruction

14 years 5 months ago
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.
Frédéric Blanqui, Jean-Pierre Jouann
Added 08 Jun 2010
Updated 08 Jun 2010
Type Conference
Year 2007
Where LPAR
Authors Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio
Comments (0)