scientific article; zbMATH DE number 2185669

MaRDI QIDQ3024845zbMATH OpenFDO

Authors François Leclerc

Publication date 4 July 2005

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

• scientific article; zbMATH DE number 408817
• Proof-theoretic analysis of termination proofs
• Coq formalization of the higher-order recursive path ordering
• An effective proof of the well-foundedness of the multiset path ordering
• Certified Higher-Order Recursive Path Ordering

Cited in

(11)

• Termination proofs by multiset path orderings imply primitive recursive derivation lengths
• CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verifications of termination certificates
• Certified Higher-Order Recursive Path Ordering
• TERMINATION OF ABSTRACT REDUCTION SYSTEMS
• scientific article; zbMATH DE number 1223620 (Why is no real title available?)
• scientific article; zbMATH DE number 2154398 (Why is no real title available?)
• Termination proofs by multiset path orderings imply primitive recursive derivation lengths
• On the formalization of termination techniques based on multiset orderings
• Admissible ordering on monomials is well-founded: a constructive proof
• 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:

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