  We revisit the static dependency pair method for proving termination of
higher-order term rewriting and extend it in a number of ways:
  (1) We introduce a new rewrite formalism designed for general applicability
in termination proving of higher-order rewriting, Algebraic Functional Systems
with Meta-variables. (2) We provide a syntactically checkable soundness
criterion to make the method applicable to a large class of rewrite systems.
(3) We propose a modular dependency pair framework for this higher-order
setting. (4) We introduce a fine-grained notion of formative and computable
chains to render the framework more powerful. (5) We formulate several existing
and new termination proving techniques in the form of processors within our
framework.
  The framework has been implemented in the (fully automatic) higher-order
termination tool WANDA.
