Pages that link to "Item:Q3183545"
From MaRDI portal
The following pages link to Certification of Termination Proofs Using CeTA (Q3183545):
Displaying 37 items.
- CeTA (Q18676) (← links)
- A learning-based fact selector for Isabelle/HOL (Q331617) (← links)
- Proving termination by dependency pairs and inductive theorem proving (Q438537) (← links)
- Reachability, confluence, and termination analysis with state-compatible automata (Q515687) (← links)
- A framework for developing stand-alone certifiers (Q530847) (← links)
- Proof certificates for equality reasoning (Q1744408) (← links)
- Multi-dimensional interpretations for termination of term rewriting (Q2055861) (← links)
- Tuple interpretations for termination of term rewriting (Q2102931) (← links)
- Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL (Q2209537) (← links)
- Certifying proofs in the first-order theory of rewriting (Q2233502) (← links)
- A Perron-Frobenius theorem for deciding matrix growth (Q2239274) (← links)
- From LCF to Isabelle/HOL (Q2280211) (← links)
- A framework for the verification of certifying computations (Q2351144) (← links)
- Proof pearl: A mechanized proof of GHC's mergesort (Q2351394) (← links)
- Analyzing program termination and complexity automatically with \textsf{AProVE} (Q2362493) (← links)
- Automatically proving termination and memory safety for programs with pointer arithmetic (Q2362494) (← links)
- Proof Pearl: regular expression equivalence and relation algebra (Q2392416) (← links)
- Automatic refinement to efficient data structures: a comparison of two approaches (Q2417948) (← links)
- Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems (Q2829264) (← links)
- Deriving Comparators and Show Functions in Isabelle/HOL (Q2945654) (← links)
- Formalizing Soundness and Completeness of Unravelings (Q2964466) (← links)
- (Q2985126) (← links)
- A Lambda-Free Higher-Order Recursive Path Order (Q2988386) (← links)
- Termination of Isabelle Functions via Termination of Rewriting (Q3088004) (← links)
- Animating the Formalised Semantics of a Java-Like Language (Q3088008) (← links)
- CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates (Q3094178) (← links)
- A Decision Procedure for Regular Expression Equivalence in Type Theory (Q3100207) (← links)
- Generalized and Formalized Uncurrying (Q3172898) (← links)
- A Mechanized Proof of Higman’s Lemma by Open Induction (Q3295156) (← links)
- Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting (Q5164173) (← links)
- Structural Rewriting in the pi-Calculus. (Q5240137) (← links)
- Formalizing Bachmair and Ganzinger's ordered resolution prover (Q5919011) (← links)
- (Q6060676) (← links)
- First-order theory of rewriting for linear variable-separated rewrite systems: automation, formalization, certification (Q6103588) (← links)
- Linear resources in Isabelle/HOL (Q6552504) (← links)
- On complexity bounds and confluence of parallel term rewriting (Q6622000) (← links)
- From innermost to full almost-sure termination of probabilistic term rewriting (Q6629527) (← links)