Certification of Termination Proofs Using CeTA
From MaRDI portal
Publication:3183545
DOI10.1007/978-3-642-03359-9_31zbMATH Open1252.68265OpenAlexW1482572800MaRDI QIDQ3183545FDOQ3183545
Authors: 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
Recommendations
Cites Work
- Title not available (Why is that?)
- Termination of term rewriting using dependency pairs
- An Efficient Unification Algorithm
- Term Rewriting and All That
- Automating the dependency pair method
- Frontiers of Combining Systems
- Logic for Programming, Artificial Intelligence, and Reasoning
- Tyrolean termination tool: techniques and features
- Certification of Automated Termination Proofs
- Certifying a Termination Criterion Based on Graphs, without Graphs
Cited In (44)
- Linear resources in Isabelle/HOL
- Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL
- First-order theory of rewriting for linear variable-separated rewrite systems: automation, formalization, certification
- Analyzing program termination and complexity automatically with \textsf{AProVE}
- A Decision Procedure for Regular Expression Equivalence in Type Theory
- Tuple interpretations for termination of term rewriting
- A framework for developing stand-alone certifiers
- Multi-dimensional interpretations for termination of term rewriting
- A Mechanized Proof of Higman’s Lemma by Open Induction
- Deriving comparators and show functions in Isabelle/HOL
- Automated certified proofs with CiME3
- Proof pearl: A mechanized proof of GHC's mergesort
- A framework for the verification of certifying computations
- Formalizing soundness and completeness of unravelings
- Proving termination by dependency pairs and inductive theorem proving
- Certifying proofs in the first-order theory of rewriting
- Formalized proof systems for propositional logic
- Formalized proofs of the infinity and normal form predicates in the first-order theory of rewriting
- Certifying confluence proofs via relative termination and rule labeling
- Certification of classical confluence results for left-linear term rewrite systems
- Certification of Automated Termination Proofs
- On complexity bounds and confluence of parallel term rewriting
- CeTA
- Finding and certifying loops
- Proof Pearl: regular expression equivalence and relation algebra
- A learning-based fact selector for Isabelle/HOL
- From innermost to full almost-sure termination of probabilistic term rewriting
- A Perron-Frobenius theorem for deciding matrix growth
- Automatically proving termination and memory safety for programs with pointer arithmetic
- Certification of nontermination proofs
- From LCF to Isabelle/HOL
- Certification of complexity proofs using CeTA
- Certifying safety and termination proofs for integer transition systems
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- Structural Rewriting in the pi-Calculus.
- A Lambda-Free Higher-Order Recursive Path Order
- Automatic refinement to efficient data structures: a comparison of two approaches
- Proof certificates for equality reasoning
- Animating the formalised semantics of a Java-like language
- 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
- Certified subterm criterion and certified usable rules
- Reachability, confluence, and termination analysis with state-compatible automata
- Generalized and formalized uncurrying
Uses Software
This page was built for publication: Certification of Termination Proofs Using CeTA
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3183545)
