The Higher-Order Recursive Path Ordering

This paper extends the termination proof techniques based on reduction orderings to a higher-order setting, by adapting the recursive path ordering definition to terms of a typed lambda-calculus generated by a signature of polymorphic higher-order function symbols. The obtained ordering is well-founded, compatible with

• Type: Conference
• Year: 1999
• Where: LICS
• Authors: Jean-Pierre Jouannaud, Albert Rubio
• Keywords: Automated Reasoning, Function Symbols, LICS 1999, Polymorphic Rewrite Rule, Polymorphic Typing