PeaCoq

IDE

A Coq-based IDE with OCaml plugin and TypeScript support

PeaCoq is a pretty Coq, isn't it?

GitHub

106 stars
8 watching
10 forks
Language: Coq
last commit: about 5 years ago
Linked from 2 awesome lists


Screenshot of Ptival/PeaCoq website

goto.ucsd.edu/peacoq

Backlinks from these awesome lists:

Related projects:

RepositoryDescriptionStars
ejgallego/coq-lspA tool for interactive theorem proving and language support in Coq153
pedrotst/coquedilleTranslates Coq terms into Cedille terms for a specific domain-specific language33
mit-plv/coqutilA collection of reusable tools and utilities for working with the Coq proof assistant42
coq/vscoqAn extension for Visual Studio Code and VSCodium to support Coq Proof Assistant349
cpitclaudel/company-coqAn Emacs plugin that enhances Coq mode with various features and tools for writing and debugging proof-based software351
lpcic/coq-elpiProvides an extension language for Coq to manipulate terms containing binders and supports scripting and metaprogramming141
jscoq/jscoqAn online development environment for the proof assistant Coq, allowing users to run and interact with it in their browser.518
ejgallego/pycoqPython bindings for Coq's interactive proof assistant50
coq-community/paramcoqA Coq plugin providing commands for generating parametricity statements used in data refinement proofs.45
smtcoq/smtcoqAn OCaml-based plugin for Coq that verifies and extends proof witnesses from external SAT/SMT solvers157
coq-community/bitsA formalization of bitset operations in Coq with extraction to OCaml native integers.22
lysxia/coq-simple-ioProvides tools to implement IO programs directly in Coq31
mit-plv/rupicolaA toolkit for compiling functional programs into imperative code for performance-critical applications51
princeton-vl/coqgymA learning environment for theorem proving with the Coq proof assistant388
unicoq/unicoqA plugin for Coq that improves its unification algorithm51