This work extends the termination proof techniques based on
reduction orderings to a higher-order setting, by defining a family
of recursive path orderings for terms of a typed lambda-calculus
generated by a signature of polymorphic higher-order function
symbols. These relations can be generated from two given
well-founded orderings, on the function symbols and on the type
constructors. The obtained orderings on terms are well-founded,
include $\beta$-reductions, are monotonic for terms of equal type,
and stable under substitution. They can be used to prove the strong
normalization property of the various existing kinds of higher-order
calculi in which constants can be defined by higher-order rewrite
rules, regardless of whether these calculi use first-order or
higher-order pattern matching. Many non-trivial examples are given
which examplify the expressive power of these orderings.
As a conclusion, we will define a single ordering integrating the
term ordering and the type ordering into a single one
operating on terms and types as well. This presentation should be
considered as the key missing stone on the way towards the
definition of a recursive path ordering for dependent type calculi.