coq-big-o
Big Complexity Notation
Provides a formalization of Big O and related notations in Coq
A general yet easy-to-use formalization of Big O, Big Theta, and more based on seminormed vector spaces.
35 stars
2 watching
1 forks
Language: Coq
last commit: almost 8 years ago big-ocomplexitycoqmathematics
Related projects:
| Repository | Description | Stars |
|---|---|---|
 coq-community/bignums | A Coq library providing support for arbitrarily large numbers | 22 |
| coq-community/bits | A formalization of bitset operations in Coq with extraction to OCaml native integers. | 22 |
 hivert/coq-combi | An algebraic combinatorics library formalized in Coq, providing a comprehensive set of functions and theories for symmetric functions. | 1 |
 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/tarjan | Formalization of Tarjan and Kosaraju's strongly connected component algorithm in Coq for finite graphs. | 13 |
| coq-community/lemma-overloading | A Coq library demonstrating design patterns for automated proof automation and canonical structures | 26 |
 math-comp/coq-combi | Formalizes algebraic combinatorics and symmetric functions in Coq. | 37 |
| coq-community/dedekind-reals | A formalization of Dedekind reals numbers in the Coq programming language | 43 |
 fblanqui/color | A comprehensive Coq library providing formal definitions and proofs of rewriting theory, lambda-calculus, and termination. | 35 |
 dmxlarchey/friedman-tree | A Coq implementation of Harvey Friedman's tree(n) function and its properties related to homeomorphic embedding. | 0 |
| coq-community/hydra-battles | Investigating various aspects of discrete mathematics and formal proofs in Coq, including ordinal numbers and computability theory. | 69 |
| coq-community/gaia | A Coq implementation of mathematical concepts from N. Bourbaki's Elements of Mathematics | 30 |
 geocoq/geocoq | A formalization of geometry using the Coq proof assistant. | 186 |
 geohot/coq-hardy | Formalizing mathematical theorems from Hardy's book in Coq to create a rigorous and reproducible formalization of number theory | 53 |