CeTA
From MaRDI portal
Cited in
(only showing first 100 items - show all)- CoqJVM
- Proof certificates for equality reasoning
- Fast machine words in Isabelle/HOL
- Tyrolean
- AProVE
- Multi-dimensional interpretations for termination of term rewriting
- Tuple interpretations for termination of term rewriting
- CSI
- CoLoR
- CiME
- MU-TERM
- mkbTT
- Slothrop
- Jambox
- Saigawa
- IsaFoR
- Matchbox
- Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL
- A Perron-Frobenius theorem for deciding matrix growth
- From LCF to Isabelle/HOL
- A verified implementation of algebraic numbers in Isabelle/HOL
- A framework for the verification of certifying computations
- Proof pearl: A mechanized proof of GHC's mergesort
- Formalizing complex plane geometry
- 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
- CSI: new evidence -- a progress report
- Certifying confluence of quasi-decreasing strongly deterministic conditional term rewrite systems
- Certifying safety and termination proofs for integer transition systems
- Automatic refinement to efficient data structures: a comparison of two approaches
- CoLL
- Ctrl
- Certification of classical confluence results for left-linear term rewrite systems
- KITTeL
- KBCV – Knuth-Bendix Completion Visualizer
- Stream Fusion for Isabelle’s Code Generator
- Deriving comparators and show functions in Isabelle/HOL
- HOL-TestGen
- Formalizing Knuth-Bendix orders and Knuth-Bendix completion
- 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
- A Decision Procedure for Regular Expression Equivalence in Type Theory
- KBCV
- Generalized and formalized uncurrying
- Proving termination of programs automatically with AProVE
- A Mechanized Proof of Higman’s Lemma by Open Induction
- A learning-based fact selector for Isabelle/HOL
- Fiat
- WorkflowFM
- SparrowBerry
- A3PAT
- Nagoya Termination Tool
- ConCon
- Code generation via higher-order rewrite systems
- term-rewriting
- EasyInterface
- CoCoWeb
- Cops
- FinFuns
- Myhill-Nerode
- Dijkstra Shortest Path
- CAVA Automata Library
- Efficient Mergesort
- Stream Fusion
- Stream Fusion Code
- Berlekamp Zassenhaus
- Perron Frobenius
- Well Quasi Orders
- Archive Formal Proofs
- Logtk
- FORT
- LLL Factorization
- Verified LLL
- Matrix Operations
- Xml
- Haskell Show Class
- Tree Automata
- Jinja not Java
- Nested Multisets
- Light-weight Containers
- LTL_to_GBA
- Coccinelle
- Real_Impl
- Maximum Cardinality Matching
- Decreasing Diagrams II
- Proving termination by dependency pairs and inductive theorem proving
- Linear Recurrences
- Count Complex Roots
- Certification_Monads
- ShortestPath
- ProTeM
- Reachability, confluence, and termination analysis with state-compatible automata
- Abstract completion, formalized
- Certification of complexity proofs using CeTA
- scientific article; zbMATH DE number 6744203 (Why is no real title available?)
- Certified rule labeling
- AC dependency pairs revisited
This page was built for software: CeTA
