A Recursive Path Ordering for Higher-Order Terms Compatible with
\beta\eta-Reductions
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 which is
compatible with \beta\eta-reductions. This ordering is powerful
enough to show the classical strong normalization property of the
simply typed \lambda-calculus extended by primitive recursion of
higher type over an abstract data type.
full paper