CeTA
From MaRDI portal
Software:18676
swMATH6584MaRDI QIDQ18676FDOQ18676
Author name not available (Why is that?)
Cited In (46)
- Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL
- Modular complexity analysis for term rewriting
- Stream Fusion for Isabelle’s Code Generator
- 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
- CSI: new evidence -- a progress report
- Title not available (Why is that?)
- A Mechanized Proof of Higman’s Lemma by Open Induction
- A verified implementation of algebraic numbers in Isabelle/HOL
- Deriving comparators and show functions in Isabelle/HOL
- Proof pearl: A mechanized proof of GHC's mergesort
- Fast machine words in Isabelle/HOL
- A framework for the verification of certifying computations
- Proving termination by dependency pairs and inductive theorem proving
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- Modular and certified semantic labeling and unlabeling
- Certified rule labeling
- Proving termination of programs automatically with AProVE
- AC dependency pairs revisited
- Certifying confluence proofs via relative termination and rule labeling
- Certification of classical confluence results for left-linear term rewrite systems
- Proof Pearl: regular expression equivalence and relation algebra
- Formalizing complex plane geometry
- Formalizing Knuth-Bendix orders and Knuth-Bendix completion
- A learning-based fact selector for Isabelle/HOL
- A Perron-Frobenius theorem for deciding matrix growth
- Automatically proving termination and memory safety for programs with pointer arithmetic
- From LCF to Isabelle/HOL
- Certification of complexity proofs using CeTA
- Certifying confluence of quasi-decreasing strongly deterministic conditional term rewrite systems
- Certifying safety and termination proofs for integer transition systems
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- Abstract completion, formalized
- A Lambda-Free Higher-Order Recursive Path Order
- KBCV – Knuth-Bendix Completion Visualizer
- Automatic refinement to efficient data structures: a comparison of two approaches
- Proof certificates for equality reasoning
- Code generation via higher-order rewrite systems
- Animating the formalised semantics of a Java-like language
- Termination of Isabelle functions via termination of rewriting
- Certified subterm criterion and certified usable rules
- Reachability, confluence, and termination analysis with state-compatible automata
- Generalized and formalized uncurrying
This page was built for software: CeTA
