Termination of rewrite relations on ?-terms based on Girard's notion of reducibility
In this paper, we show how to extend the notion of reducibility introduced by Girard for proving the termination of ?-reduction in the polymorphic ?-calculus, to prove the termination of various kinds of rewrite relations on ?-terms, including rewriting modulo some equational theory and rewriting with matching modulo ??, by using the notion of computability closure. This provides a powerful termination criterion for various higher-order rewriting frameworks, including Klop's Combinatory Reductions Systems with simple types and Nipkow's Higher-order Rewrite Systems.
termination rewriting ?-calculus rewriting modulo matching modulo ?? types girard's reducibility patterns  la miller