Higher-Order Orderings for Normal Rewriting

DOI10.1007/11805618_29MaRDI QIDQ3527310zbMATH OpenOpenAlexFDO

Authors Jean-Pierre Jouannaud, Albert Rubio

Publication date 25 September 2008

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11805618_29

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

• Normal higher-order termination
• A termination ordering for higher order rewrite systems
• Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering
• A recursive path ordering for higher-order terms in η-long β-normal form
• Polymorphic higher-order recursive path orderings

Cited in

(15)

• Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering
• Proof theory of higher-order equations: Conservativity, normal forms and term rewriting.
• Order-Sorted Rewriting and Congruence Closure
• Normal higher-order termination
• scientific article; zbMATH DE number 2185672 (Why is no real title available?)
• The Computability Path Ordering: The End of a Quest
• Bi-rewriting, a term rewriting technique for monotonic order relations
• A termination ordering for higher order rewrite systems
• A recursive path ordering for higher-order terms in η-long β-normal form
• Polynomial interpretations for higher-order rewriting
• First-order formative rules
• Natural inductive theorems for higher-order rewriting
• Processes, Terms and Cycles: Steps on the Road to Infinity
• Coq formalization of the higher-order recursive path ordering
• Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility

Describes a project that uses

Uses Software

• Isabelle

This page was built for publication: Higher-Order Orderings for Normal Rewriting

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3527310)