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