Polymorphic higher-order recursive path orderings

DOI10.1145/1206035.1206037zbMath1312.68040OpenAlexW1986072156MaRDI QIDQ3546327

Jean-Pierre Jouannaud, Albert Rubio

Publication date: 21 December 2008

Published in: Journal of the ACM (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/1206035.1206037

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40)

Related Items (15)

Coq formalization of the higher-order recursive path ordering ⋮ Uncurrying for termination and complexity ⋮ Size-based termination of higher-order rewriting ⋮ Normal Higher-Order Termination ⋮ HORPO with Computability Closure: A Reconstruction ⋮ Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility ⋮ Termination Proof of S-Expression Rewriting Systems with Recursive Path Relations ⋮ A Lambda-Free Higher-Order Recursive Path Order ⋮ The Computability Path Ordering: The End of a Quest ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Superposition with lambdas ⋮ Superposition with lambdas ⋮ The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type ⋮ A Knuth-Bendix-like ordering for orienting combinator equations

This page was built for publication: Polymorphic higher-order recursive path orderings