Certification of Termination Proofs Using CeTA
From MaRDI portal
Recommendations
Cites work
- 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
- scientific article; zbMATH DE number 1952947 (Why is no real title available?)
- 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
(73)- Proof certificates for equality reasoning
- CeTA
- Multi-dimensional interpretations for termination of term rewriting
- Tuple interpretations for termination of term rewriting
- Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL
- Certifying proofs in the first-order theory of rewriting
- A Perron-Frobenius theorem for deciding matrix growth
- From LCF to Isabelle/HOL
- A framework for the verification of certifying computations
- Proof pearl: A mechanized proof of GHC's mergesort
- Analyzing program termination and complexity automatically with \textsf{AProVE}
- Automatically proving termination and memory safety for programs with pointer arithmetic
- Proof Pearl: regular expression equivalence and relation algebra
- Certifying safety and termination proofs for integer transition systems
- Automatic refinement to efficient data structures: a comparison of two approaches
- Certification of classical confluence results for left-linear term rewrite systems
- Certification of nontermination proofs
- Deriving comparators and show functions in Isabelle/HOL
- Formalizing soundness and completeness of unravelings
- Certifying confluence proofs via relative termination and rule labeling
- A Lambda-Free Higher-Order Recursive Path Order
- Termination of Isabelle functions via termination of rewriting
- Animating the formalised semantics of a Java-like language
- CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verifications of termination certificates
- A Decision Procedure for Regular Expression Equivalence in Type Theory
- Generalized and formalized uncurrying
- A Mechanized Proof of Higman’s Lemma by Open Induction
- A learning-based fact selector for Isabelle/HOL
- Finding and certifying loops
- Certification of Automated Termination Proofs
- Proving termination by dependency pairs and inductive theorem proving
- 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
- Structural rewriting in the pi-calculus
- Certification of complexity proofs using CeTA
- A framework for developing stand-alone certifiers
- Automated certified proofs with CiME3
- Certified subterm criterion and certified usable rules
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- Formalized proof systems for propositional logic
- First-order theory of rewriting for linear variable-separated rewrite systems: automation, formalization, certification
- Linear resources in Isabelle/HOL
- On complexity bounds and confluence of parallel term rewriting
- From innermost to full almost-sure termination of probabilistic term rewriting
- Wanda -- a higher-order termination tool (system description)
- Certifying the weighted path order (invited talk)
- From innermost to full probabilistic term rewriting: almost-sure termination, complexity, and modularity
- A modular formalization of superposition in Isabelle/HOL
- Impredicativity, cumulativity and product covariance in the logical framework dedukti
- An Isabelle/HOL formalization of semi-Thue and conditional semi-Thue systems
- Linear Inequalities
- A Formalization of Knuth–Bendix Orders
- Polynomial Factorization
- Computing N-th Roots using the Babylonian Method
- Perron-Frobenius Theorem for Spectral Radius Analysis
- Executable Matrix Operations on Matrices of Arbitrary Dimensions
- Implementing field extensions of the form Q[sqrt(b)]
- First-Order Rewriting
- Executable Transitive Closures of Finite Relations
- Sorted Rewriting, Conditional Rewriting, and Logically Constrained Rewriting
- Abstract Rewriting
- Executable Transitive Closures
- Matrices, Jordan Normal Forms, and Spectral Radius Theory
- Generating linear orders for datatypes
- Lifting Definition Option
- Executable Multivariate Polynomials
- Deriving class instances for datatypes
- Algebraic Numbers in Isabelle/HOL
- Complete Non-Orders and Fixed Points
- Polynomial Interpolation
- The Factorization Algorithm of Berlekamp and Zassenhaus
- A Formalization of Weighted Path Orders and Recursive Path Orders
- First-Order Terms
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)
