pycoq
Proof assistant library
Python bindings for Coq's interactive proof assistant
Python bindings for the Coq interactive proof assistant
50 stars
4 watching
4 forks
Language: OCaml
last commit: about 3 years ago
Linked from 1 awesome list
coqmachine-learningpythonverification
Related projects:
| Repository | Description | Stars |
|---|---|---|
| ejgallego/coq-lsp | A tool for interactive theorem proving and language support in Coq | 153 |
 princeton-vl/coqgym | A learning environment for theorem proving with the Coq proof assistant | 388 |
 whonore/coqtail | Enables interactive proof development in Vim similar to other proof assistants. | 274 |
 coq/vscoq | An extension for Visual Studio Code and VSCodium to support Coq Proof Assistant | 349 |
 eugeneloy/coq_jupyter | A Jupyter notebook kernel for interactive theorem proving with Coq | 94 |
 coq-community/coq-art | Coq proof assistant book with exercises and examples | 114 |
| coq/platform | A multi-platform distribution of the Coq proof assistant and its libraries, providing a standardized setup for development and teaching | 191 |
 formal-land/coq-of-python | Formal verification of Python code using Coq | 30 |
| coq-community/lemma-overloading | A Coq library demonstrating design patterns for automated proof automation and canonical structures | 26 |
 uwplse/structtact | A Coq library providing structural tactics and utility definitions to simplify proof development in proof assistants. | 21 |
 ilyasergey/pnp | A tutorial project on using Coq to mechanize mathematics with dependent types | 160 |
 engineeringsoftware/mcoq | Analyze and test Coq proof assistant projects by generating modified versions of the code to identify flaws in specifications. | 30 |
 math-comp/coq-combi | Formalizes algebraic combinatorics and symmetric functions in Coq. | 37 |
 jwiegley/coq-haskell | A Coq library providing definitions and notations to facilitate interaction between Haskell developers and the Coq proof assistant. | 168 |