HORPO with Computability Closure : A Reconstruction
This paper provides a new, decidable definition of the higher-order
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.
extended abstract