The Computability Path Ordering: The End of a Quest

DOI10.1007/978-3-540-87531-4_1zbMath1156.68568OpenAlexW1558388494MaRDI QIDQ3540166

Albert Rubio, Jean-Pierre Jouannaud, Frédéric Blanqui

Publication date: 20 November 2008

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

Full work available at URL: https://hal.inria.fr/inria-00288209v2/file/main.pdf

Mathematics Subject Classification ID

Logic in computer science (03B70) Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42)

Related Items

Harnessing First Order Termination Provers Using Higher Order Dependency Pairs, Normal Higher-Order Termination, Jumping and escaping: modular termination and the abstract path ordering, Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility, Simplifying Algebraic Functional Systems, A Knuth-Bendix-like ordering for orienting combinator equations

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Orderings for term-rewriting systems
• On recursive path ordering
• Adding algebraic rewriting to the untyped lambda calculus
• Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering
• Abstract data type systems
• Dependent types for program termination verification
• Termination of term rewriting using dependency pairs
• A Monotonic Higher-Order Semantic Path Ordering
• HORPO with Computability Closure: A Reconstruction
• Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages
• Higher-Order Orderings for Normal Rewriting
• Polymorphic higher-order recursive path orderings
• Orderings and Constraints: Theory and Practice of Proving Termination
• Computability Closure: Ten Years Later
• Modularity of strong normalization in the algebraic-λ-cube
• Termination of rewriting in the Calculus of Constructions
• Type-based termination of recursive definitions
• Definitions by rewriting in the Calculus of Constructions
• Termination checking with types
• The size-change principle for program termination
• Higher-Order Termination: From Kruskal to Computability
• Logic for Programming, Artificial Intelligence, and Reasoning
• Termination of combined (rewrite and λ-calculus) systems
• Adding algebraic rewriting to the calculus of constructions : Strong normalization preserved
• Rewriting Techniques and Applications
• Rewriting Techniques and Applications
• Inductive-data-type systems
• Calculating sized types