CeTA
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Abstract completion, formalized
- A Lambda-Free Higher-Order Recursive Path Order
- NaTT
- Automatic refinement to efficient data structures: a comparison of two approaches
- KBCV – Knuth-Bendix Completion Visualizer
- Proof certificates for equality reasoning
- Animating the formalised semantics of a Java-like language
- Code generation via higher-order rewrite systems
- Termination of Isabelle functions via termination of rewriting
- Reachability, confluence, and termination analysis with state-compatible automata
- Robinson arithmetic
- Certified subterm criterion and certified usable rules
- Generalized and formalized uncurrying
- Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL
- Modular complexity analysis for term rewriting
- A framework for developing stand-alone certifiers
- Stream Fusion for Isabelle’s Code Generator
- 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
- CSI: new evidence -- a progress report
- scientific article; zbMATH DE number 6744203 (Why is no real title available?)
- 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
- CoqJVM
- AProVE
- Tyrolean
- CSI
- CoLoR
- CiME
- mkbTT
- Jambox
- MU-TERM
- IsaFoR
- Matchbox
- Slothrop
- Saigawa
- CoLL
- Ctrl
- KITTeL
- HOL-TestGen
- Matrix Operations
- KBCV
- Fiat
- A3PAT
- ConCon
- Nagoya Termination Tool
- SparrowBerry
- WorkflowFM
- EasyInterface
- term-rewriting
- CoCoWeb
- Cops
- CAVA Automata Library
- Archive Formal Proofs
- Berlekamp Zassenhaus
- Dijkstra Shortest Path
- FinFuns
- Efficient Mergesort
- FORT
- Myhill-Nerode
- Logtk
- LLL Factorization
- Perron Frobenius
- Haskell Show Class
- Jinja not Java
- Nested Multisets
- Coccinelle
- Light-weight Containers
- LTL_to_GBA
- Decreasing Diagrams II
- Stream Fusion
- Stream Fusion Code
- Real_Impl
- Well Quasi Orders
- Verified LLL
- Maximum Cardinality Matching
- Tree Automata
- Xml
- Count Complex Roots
- Certification_Monads
- Linear Recurrences
- ShortestPath
- ProTeM
- Open Induction
- Saturation_Framework
- TcT
- AC dependency pairs revisited
- Certifying confluence proofs via relative termination and rule labeling
- Certification of classical confluence results for left-linear term rewrite systems
This page was built for software: CeTA
