CoLoR
From MaRDI portal
Cited in
(70)- Formally proving size optimality of sorting networks
- CeTA
- HOCL
- Tyrolean
- AProVE
- RALL
- Multi-dimensional interpretations for termination of term rewriting
- Tuple interpretations for termination of term rewriting
- CSI
- CiME
- Jambox
- Saigawa
- IsaFoR
- TPA
- Matchbox
- Formally verifying the solution to the Boolean Pythagorean triples problem
- Analyzing program termination and complexity automatically with \textsf{AProVE}
- Automatically proving termination and memory safety for programs with pointer arithmetic
- Certifying confluence of quasi-decreasing strongly deterministic conditional term rewrite systems
- Certifying safety and termination proofs for integer transition systems
- CoLL
- Certification of classical confluence results for left-linear term rewrite systems
- Deciding Kleene algebras in \texttt{Coq}
- KITTeL
- A Lambda-Free Higher-Order Recursive Path Order
- Max/Plus tree automata for termination of term rewriting
- Point-free, set-free concrete linear algebra
- Termination of Isabelle functions via termination of rewriting
- Generalized and formalized uncurrying
- Acyclic Preferences and Existence of Sequential Nash Equilibria: A Formal and Constructive Equivalence
- Certification of Termination Proofs Using CeTA
- Proving termination of programs automatically with AProVE
- SparrowBerry
- A3PAT
- Nagoya Termination Tool
- ConCon
- Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
- A formalization of Newman's and Yokouchi's lemmas in a higher-order language
- Certifying a Termination Criterion Based on Graphs, without Graphs
- Modeling Permutations in Coq for Coccinelle
- Automatic Termination
- CoCoWeb
- Cops
- Knuth Bendix Orders
- Equations
- ATBR
- SAEPTUM
- FELIX
- Lambda Free RPOs
- Xml
- Haskell Show Class
- RRL
- Coccinelle
- Certification_Monads
- Solving graph partitioning problems with parallel metaheuristics
- Syntactic soundness proof of a type-and-capability system with hidden state
- Mechanically certifying formula-based Noetherian induction reasoning
- scientific article; zbMATH DE number 7204430 (Why is no real title available?)
- A PVS theory for term rewriting systems
- scientific article; zbMATH DE number 6744203 (Why is no real title available?)
- A framework for developing stand-alone certifiers
- Certified subterm criterion and certified usable rules
- Certification of Proving Termination of Term Rewriting by Matrix Interpretations
- An efficient Coq tactic for deciding Kleene algebras
- Preface to the special issue: Interactive theorem proving and the formalization of mathematics
- NaTT
- WANDA
- A formalization of the Knuth-Bendix(-Huet) critical pair theorem
- Coq formalization of the higher-order recursive path ordering
- An effective proof of the well-foundedness of the multiset path ordering
This page was built for software: CoLoR
