PeaCoq
IDE
A Coq-based IDE with OCaml plugin and TypeScript support
PeaCoq is a pretty Coq, isn't it?
106 stars
8 watching
10 forks
Language: Coq
last commit: over 3 years ago
Linked from 2 awesome lists
uhub/awesome-coq
awesomo4000/awesome-provableRelated projects:
| Repository | Description | Stars |
|---|---|---|
 ejgallego/coq-lsp | A tool for interactive theorem proving and language support in Coq | 152 |
 pedrotst/coquedille | Translates Coq terms into Cedille terms for a specific domain-specific language | 33 |
 mit-plv/coqutil | A collection of reusable tools and utilities for working with the Coq proof assistant | 41 |
 coq/vscoq | A Visual Studio Code extension for Coq proof assistant support | 343 |
 cpitclaudel/company-coq | An Emacs plugin that enhances Coq mode with various features and tools for writing and debugging proof-based software | 354 |
 lpcic/coq-elpi | A Coq plugin embedding Elpi to extend Coq's capabilities with a dialect of lambda-prolog for metaprogramming and scripting. | 139 |
 jscoq/jscoq | An online development environment for the proof assistant Coq, allowing users to run and interact with it in their browser. | 515 |
| ejgallego/pycoq | Python bindings for Coq's interactive proof assistant | 50 |
 coq-community/paramcoq | A Coq plugin providing commands for generating parametricity statements used in data refinement proofs. | 44 |
 smtcoq/smtcoq | An OCaml-based plugin for Coq that verifies and extends proof witnesses from external SAT/SMT solvers | 156 |
| coq-community/bits | A formalization of bitset operations in Coq with extraction to OCaml native integers. | 22 |
 lysxia/coq-simple-io | Provides tools to implement IO programs directly in Coq | 31 |
| mit-plv/rupicola | A toolkit for compiling functional programs into imperative code for performance-critical applications | 50 |
 princeton-vl/coqgym | A learning environment for theorem proving with the Coq proof assistant | 384 |
 unicoq/unicoq | An enhanced unification algorithm for Coq | 49 |