Certification of Automated Termination Proofs

DOI10.1007/978-3-540-74621-8_10zbMath1148.68465OpenAlexW1541688478MaRDI QIDQ3525007

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

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)

Related Items

Coq formalization of the higher-order recursive path ordering, Certification of Termination Proofs Using CeTA, A formalization of the Knuth-Bendix(-Huet) critical pair theorem, Mechanical certification of \(\mathrm{FOL_{ID}}\) cyclic proofs, Certifying a Termination Criterion Based on Graphs, without Graphs, Mechanically certifying formula-based Noetherian induction reasoning, Incorporating quotation and evaluation into Church's type theory, A PVS Theory for Term Rewriting Systems, Certification of Proving Termination of Term Rewriting by Matrix Interpretations, Unnamed Item, Termination of Isabelle Functions via Termination of Rewriting, CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates, Automated Certification of Implicit Induction Proofs, Automated verification of refinement laws, Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme

Uses Software

• Coq