Certification of Termination Proofs Using CeTA

DOI10.1007/978-3-642-03359-9_31zbMath1252.68265OpenAlexW1482572800MaRDI QIDQ3183545

René Thiemann, Christian Sternagel

Publication date: 20 October 2009

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-03359-9_31

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Grammars and rewriting systems (68Q42)

Related Items

Analyzing program termination and complexity automatically with \textsf{AProVE} ⋮ Automatically proving termination and memory safety for programs with pointer arithmetic ⋮ Unnamed Item ⋮ Generalized and Formalized Uncurrying ⋮ A learning-based fact selector for Isabelle/HOL ⋮ Proof Pearl: regular expression equivalence and relation algebra ⋮ Deriving Comparators and Show Functions in Isabelle/HOL ⋮ Automatic refinement to efficient data structures: a comparison of two approaches ⋮ First-order theory of rewriting for linear variable-separated rewrite systems: automation, formalization, certification ⋮ Formalizing Soundness and Completeness of Unravelings ⋮ Proving termination by dependency pairs and inductive theorem proving ⋮ Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL ⋮ Unnamed Item ⋮ Structural Rewriting in the pi-Calculus. ⋮ A Lambda-Free Higher-Order Recursive Path Order ⋮ A Mechanized Proof of Higman’s Lemma by Open Induction ⋮ Certifying proofs in the first-order theory of rewriting ⋮ A Perron-Frobenius theorem for deciding matrix growth ⋮ Proof certificates for equality reasoning ⋮ Reachability, confluence, and termination analysis with state-compatible automata ⋮ Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting ⋮ A framework for developing stand-alone certifiers ⋮ From LCF to Isabelle/HOL ⋮ Formalizing Bachmair and Ganzinger's ordered resolution prover ⋮ Termination of Isabelle Functions via Termination of Rewriting ⋮ Animating the Formalised Semantics of a Java-Like Language ⋮ Multi-dimensional interpretations for termination of term rewriting ⋮ CeTA ⋮ CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates ⋮ Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems ⋮ A Decision Procedure for Regular Expression Equivalence in Type Theory ⋮ Tuple interpretations for termination of term rewriting ⋮ A framework for the verification of certifying computations ⋮ Proof pearl: A mechanized proof of GHC's mergesort

Uses Software

• Isabelle
• Isabelle/HOL
• Haskell
• Tyrolean
• AProVE
• CoLoR
• Matchbox

Cites Work

• Tyrolean termination tool: techniques and features
• Termination of term rewriting using dependency pairs
• Automating the dependency pair method
• Certification of Automated Termination Proofs
• Certifying a Termination Criterion Based on Graphs, without Graphs
• An Efficient Unification Algorithm
• Term Rewriting and All That
• Frontiers of Combining Systems
• Logic for Programming, Artificial Intelligence, and Reasoning
• Unnamed Item

This page was built for publication: Certification of Termination Proofs Using CeTA