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