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)- Generalized and formalized uncurrying
- Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL
- Linear resources in Isabelle/HOL
- First-order theory of rewriting for linear variable-separated rewrite systems: automation, formalization, certification
- A framework for developing stand-alone certifiers
- Analyzing program termination and complexity automatically with \textsf{AProVE}
- Tuple interpretations for termination of term rewriting
- Multi-dimensional interpretations for termination of term rewriting
- A Decision Procedure for Regular Expression Equivalence in Type Theory
- A Mechanized Proof of Higman’s Lemma by Open Induction
- Deriving comparators and show functions in Isabelle/HOL
- Proof pearl: A mechanized proof of GHC's mergesort
- Automated certified proofs with CiME3
- A framework for the verification of certifying computations
- Proving termination by dependency pairs and inductive theorem proving
- Formalizing soundness and completeness of unravelings
- 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
- CeTA
- 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
- Finding and certifying loops
- A learning-based fact selector for Isabelle/HOL
- Proof Pearl: regular expression equivalence and relation algebra
- A Perron-Frobenius theorem for deciding matrix growth
- From innermost to full almost-sure termination of probabilistic term rewriting
- 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
- Reachability, confluence, and termination analysis with state-compatible automata
- Certified subterm criterion and certified usable rules
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)
