Certified Higher-Order Recursive Path Ordering

DOI10.1007/11805618_17MaRDI QIDQ3527297zbMATH OpenOpenAlexFDO

Authors Adam Koprowski

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_17

Mathematics Subject Classification ID

Recommendations

• Coq formalization of the higher-order recursive path ordering
• A Lambda-Free Higher-Order Recursive Path Order
• Termination proof of term rewriting system with the multiset path ordering. A complete development in the system Coq
• The computability path ordering
• Polymorphic higher-order recursive path orderings

Cited in

(11)

• An improved general path order
• A Lambda-Free Higher-Order Recursive Path Order
• A Monotonic Higher-Order Semantic Path Ordering
• Termination proof of term rewriting system with the multiset path ordering. A complete development in the system Coq
• CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verifications of termination certificates
• HORPO with Computability Closure: A Reconstruction
• Polymorphic higher-order recursive path orderings
• Recursive Path Orderings Can Also Be Incremental
• A Higher-Order Iterative Path Ordering
• Coq formalization of the higher-order recursive path ordering
• An effective proof of the well-foundedness of the multiset path ordering

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Certified Higher-Order Recursive Path Ordering

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