Rewrite orderings for higher-order terms in eta-long beta-normal form and the recursive path ordering
This paper extends the termination proof techniques based on rewrite orderings to a higher-order setting, by defining a recursive path ordering for simply typed higher-order terms in long beta-normal form. This ordering is powerful enough to show termination of several complex examples. (C) 1998-Elsevier Science B.V. All rights reserved.
higher-order rewriting typed lambda calculus termination orderings