coq-course
Coq course
A self-reading Coq course for PhD students covering fundamental topics in functional programming and formal verification.
Coq course at Chalmers CSE
38 stars
14 watching
10 forks
Language: Coq
last commit: over 7 years ago Related projects:
| Repository | Description | Stars |
|---|---|---|
 princetonuniversity/vst | A collection of formal verification tools and libraries for writing secure and reliable software using the Coq proof assistant | 444 |
 princeton-vl/coqgym | A learning environment for theorem proving with the Coq proof assistant | 388 |
 ejgallego/coq-lsp | A tool for interactive theorem proving and language support in Coq | 153 |
 thery/flocqlecture | An introductory course on floating-point numbers and formal proof using Coq | 6 |
 coq-community/semantics | A comprehensive survey of programming language semantics styles implemented in Coq | 46 |
 anton-trunov/coq-lecture-notes | Lecture notes and resources for learning the Coq proof assistant | 50 |
 xavierleroy/cdf-mech-sem | Development of formal semantics and verification tools for imperative languages and functional programming languages. | 64 |
 mgrabovsky/fm-notes | A collection of notes and resources on formal methods, type theory, and theorem proving using Coq. | 21 |
 dschepler/coq-sequent-calculus | Formalizations of logical deduction systems using Coq | 44 |
 ilyasergey/pnp | A tutorial project on using Coq to mechanize mathematics with dependent types | 160 |
 jscoq/jscoq | An online development environment for the proof assistant Coq, allowing users to run and interact with it in their browser. | 518 |
 math-comp/tutorial_material | Tutorials and materials for teaching Coq-based mathematical component development | 17 |
| xavierleroy/cdf-program-logics | Companion Coq development for teaching program logics | 40 |
| coq-community/tarjan | Formalization of Tarjan and Kosaraju's strongly connected component algorithm in Coq for finite graphs. | 13 |