coinduction
Coinduction library
A library that enables formal proofs using enhanced coinduction techniques
coinduction library for Coq
15 stars
2 watching
4 forks
Language: Coq
last commit: about 1 year ago
Linked from 1 awesome list
Related projects:
| Repository | Description | Stars |
|---|---|---|
 snu-sf/paco | A Coq library for proving properties about stateful systems through parameterized coinduction | 43 |
| damien-pous/relation-algebra | A library providing modular and axiom-free decision procedures for relation algebra theories in Coq. | 48 |
 dmxlarchey/coq-kruskal | A comprehensive library of constructive Coq proofs for Kruskal's tree theorem and related concepts. | 0 |
 charguer/tlc | A Coq library providing an alternative set of axioms and type class mechanisms for building and proving mathematical theorems. | 38 |
 coq-community/corn | A comprehensive formalization of mathematical structures and concepts for verified computation in Coq. | 111 |
 dschepler/coq-sequent-calculus | Formalizations of logical deduction systems using Coq | 44 |
| coq-community/coqeal | A Coq library providing algebraic data structures and algorithms | 67 |
 jtassarotti/coq-proba | A Coq-based probability theory library providing results and definitions for discrete probability, measure theory, and probabilistic choice monads. | 50 |
| coq-community/coqtail-math | A collection of mathematical theorems and tools within the Coq proof assistant | 15 |
| coq-community/math-classes | A library of abstract interfaces for various mathematical structures to facilitate algebraic manipulation and type class-based reasoning in Coq | 162 |
 fblanqui/color | A comprehensive Coq library providing formal definitions and proofs of rewriting theory, lambda-calculus, and termination. | 35 |
| coq-community/reglang | Provides definitions and verified translations between various representations of regular languages in the Coq proof assistant | 41 |
 stepchowfun/proofs | A personal repository of formally verified mathematics using the Coq proof assistant | 292 |
| coq-community/bits | A formalization of bitset operations in Coq with extraction to OCaml native integers. | 22 |
 mit-plv/coqutil | A collection of reusable tools and utilities for working with the Coq proof assistant | 42 |