fm-notes
Coq handbook
A collection of notes and resources on formal methods, type theory, and theorem proving using Coq.
Unassorted scribbles on formal methods, type theory, category theory, and so on, and so on
20 stars
3 watching
2 forks
Language: Coq
last commit: 9 months ago coqdependent-typesformal-methodsformal-verificationhandbooklecture-notesscribblestheorem-proving
Related projects:
| Repository | Description | Stars |
|---|---|---|
 anton-trunov/coq-lecture-notes | Lecture notes and resources for learning the Coq proof assistant | 50 |
 ilyasergey/pnp | A tutorial project on using Coq to mechanize mathematics with dependent types | 160 |
 matafou/libhyps | A Coq library providing tactics to manipulate hypotheses in formal proofs. | 20 |
 stepchowfun/proofs | A personal repository of formally verified mathematics using the Coq proof assistant | 291 |
 charguer/tlc | A Coq library providing an alternative set of axioms and type class mechanisms for building and proving mathematical theorems. | 38 |
 math-comp/abel | Formalization of mathematical theorems about solvability and Galois theory for polynomials | 28 |
 geohot/coq-hardy | Formalizing mathematical theorems from Hardy's book in Coq to create a rigorous and reproducible formalization of number theory | 53 |
 choukh/set-theory | A formalization of set theory and its foundational axioms in the Coq proof assistant language | 59 |
| choukh/baby-set-theory | A Coq-based tutorial on set theory and theorem-proving using formalized mathematical proofs | 43 |
 vlopezj/coq-course | A self-reading Coq course for PhD students covering fundamental topics in functional programming and formal verification. | 38 |
 coq-community/lemma-overloading | A Coq library demonstrating design patterns for automated proof automation and canonical structures | 26 |
 princeton-vl/coqgym | A learning environment for theorem proving with the Coq proof assistant | 384 |
 thery/flocqlecture | An introductory course on formalizing floating-point numbers and their applications in Coq | 6 |