tree-calculus
Tree Calculus Proofs
Provides Coq proofs for a book on tree calculus-based programming
Proofs in Coq for the book Reflective Programs in Tree Calculus
51 stars
3 watching
4 forks
Language: Coq
last commit: over 3 years ago Related projects:
| Repository | Description | Stars |
|---|---|---|
 dmxlarchey/kruskal-veldman | A detailed proof of Wim Veldman's tree theorem adaptation in Coq | 0 |
 google/tree-math | A library that provides mathematical operations for JAX pytrees. | 188 |
 formal-land/coq-bonsai | Generates a random Coq program with a graphical tree-like structure | 24 |
 whonore/coqtail | Enables interactive proof development in Vim similar to other proof assistants. | 274 |
 math-comp/coq-combi | Formalises algebraic combinatorics in Coq using symmetric functions and polynomials | 36 |
 coq-community/fourcolor | A formal proof of a fundamental result in graph theory using the Coq proof assistant | 166 |
 ejgallego/pycoq | Python bindings for Coq's interactive proof assistant | 50 |
 fblanqui/color | A comprehensive Coq library providing formal definitions and proofs of rewriting theory, lambda-calculus, and termination. | 35 |
| dmxlarchey/coq-kruskal | A comprehensive library of constructive Coq proofs for Kruskal's tree theorem and related concepts. | 0 |
| coq-community/fav-ssr | A comprehensive library of verified data structures and algorithms in Coq | 45 |
| coq-community/coq-100-theorems | Repository tracking famous theorems proved using proof assistants. | 55 |
 hivert/coq-combi | Formalizes algebraic combinatorics in Coq with an emphasis on symmetric functions and their properties. | 1 |
 pa-ba/calc-comp | Formalizations of compiler design and virtual machine calculations in Coq | 30 |
| coq-community/coq-art | Coq proof assistant book with exercises and examples | 110 |