Certification of Automated Termination Proofs

DOI10.1007/978-3-540-74621-8_10MaRDI QIDQ3525007zbMATH OpenOpenAlexFDO

Authors Evelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, Xavier Urbain

Publication date 16 September 2008

Published in Frontiers of Combining Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-74621-8_10

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

• Automated certified proofs with CiME3
• Certification of Termination Proofs Using CeTA
• Certification of complexity proofs using CeTA
• Certification of nontermination proofs
• Certification of Proving Termination of Term Rewriting by Matrix Interpretations

Cited in

(21)

• Automated verification of refinement laws
• Incorporating quotation and evaluation into Church's type theory
• Certification of nontermination proofs
• Termination of Isabelle functions via termination of rewriting
• CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verifications of termination certificates
• Automated Certification of Implicit Induction Proofs
• Certification of Termination Proofs Using CeTA
• Certifying a Termination Criterion Based on Graphs, without Graphs
• Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
• scientific article; zbMATH DE number 107881 (Why is no real title available?)
• Mechanically certifying formula-based Noetherian induction reasoning
• scientific article; zbMATH DE number 7204430 (Why is no real title available?)
• A PVS theory for term rewriting systems
• Certification of complexity proofs using CeTA
• Automated certified proofs with CiME3
• Certification of Proving Termination of Term Rewriting by Matrix Interpretations
• Mechanical certification of \(\mathrm{FOL_{ID}}\) cyclic proofs
• A formalization of the Knuth-Bendix(-Huet) critical pair theorem
• Certifying the weighted path order (invited talk)
• From innermost to full probabilistic term rewriting: almost-sure termination, complexity, and modularity
• Coq formalization of the higher-order recursive path ordering

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Certification of Automated Termination Proofs

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