The Computability Path Ordering: The End of a Quest

DOI10.1007/978-3-540-87531-4_1MaRDI QIDQ3540166zbMATH OpenOpenAlexFDO

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

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

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

Recommendations

• The computability path ordering
• A termination ordering for higher order rewrite systems
• HORPO with Computability Closure: A Reconstruction
• A Higher-Order Iterative Path Ordering
• A recursive path ordering for higher-order terms in η-long β-normal form

Cites work

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

Cited in

(14)

• Jumping and escaping: modular termination and the abstract path ordering
• A Knuth-Bendix-like ordering for orienting combinator equations
• Normal higher-order termination
• Simplifying algebraic functional systems
• Harnessing first order termination provers using higher order dependency pairs
• The computability path ordering
• HORPO with Computability Closure: A Reconstruction
• Computability Closure: Ten Years Later
• Can One Escape Red Chains?
• Higher-Order Termination: From Kruskal to Computability
• A Simplified Application of Howard’s Vector Notation System to Termination Proofs for Typed Lambda-Calculus Systems
• Wanda -- a higher-order termination tool (system description)
• Higher-order constrained dependency pairs for (universal) computability
• Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility

This page was built for publication: The Computability Path Ordering: The End of a Quest

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