ClairvoyanceMonad
Clairvoyance framework
Formalizes reasoning about lazy computation costs using a simple framework
The Coq formalization of the paper Reasoning about the garden of forking paths.
24 stars
6 watching
2 forks
Language: Coq
last commit: 5 months ago Related projects:
| Repository | Description | Stars |
|---|---|---|
 matafou/libhyps | A Coq library providing tactics to manipulate hypotheses in formal proofs. | 20 |
 plclub/lngen | Tool for generating Coq definitions and proofs for locally nameless representations | 30 |
 coq-community/fav-ssr | A comprehensive library of verified data structures and algorithms in Coq | 45 |
| coq-community/alea | A library for reasoning about randomized algorithms in Coq | 25 |
 ejgallego/coq-lsp | A tool for interactive theorem proving and language support in Coq | 152 |
 fblanqui/color | A comprehensive Coq library providing formal definitions and proofs of rewriting theory, lambda-calculus, and termination. | 35 |
 affeldt-aist/monae | A Coq library for formalizing and reasoning about monads with equational logic | 68 |
| affeldt-aist/infotheo | A Coq formalization of mathematical foundations for information theory and error-correcting codes | 64 |
| coq-community/tarjan | Formalization of Tarjan and Kosaraju's strongly connected component algorithm in Coq for finite graphs. | 13 |
 princeton-vl/coqgym | A learning environment for theorem proving with the Coq proof assistant | 384 |
 unimath/unimath | Formalizes mathematics using the univalent point of view | 961 |
| coq-community/hydra-battles | Investigating various aspects of discrete mathematics and formal proofs in Coq, including ordinal numbers and computability theory. | 68 |
 formal-land/coq-bonsai | Generates a random Coq program with a graphical tree-like structure | 24 |
| coq-community/chapar | A framework for verifying causal consistency in distributed key-value stores and their clients using the Coq proof assistant | 32 |
 snu-sf/paco | A Coq library for proving properties about stateful systems through parameterized coinduction | 43 |