Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering

DOI10.1016/S0304-3975(98)00078-4zbMath0912.68103OpenAlexW2033042203MaRDI QIDQ1275015

Jean-Pierre Jouannaud, Albert Rubio

Publication date: 12 January 1999

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0304-3975(98)00078-4

zbMATH Keywords

higher-order rewritingtyped lambda calculustermination orderings

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items (5)

Superposition for higher-order logic ⋮ Unnamed Item ⋮ The Computability Path Ordering: The End of a Quest ⋮ Superposition with lambdas ⋮ Superposition with lambdas

Uses Software

• Automath
• RRL

Cites Work

• Orderings for term-rewriting systems
• Termination of rewriting
• Abstract data type systems
• Modularity of strong normalization in the algebraic-λ-cube
• A termination ordering for higher order rewrite systems
• Termination of combined (rewrite and λ-calculus) systems
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering