platform
Proof assistant distribution
A multi-platform distribution of the Coq proof assistant and its libraries, providing a standardized setup for development and teaching
Multi platform setup for Coq, Coq libraries and tools
191 stars
8 watching
50 forks
Language: Shell
last commit: 3 months ago
Linked from 1 awesome list
Related projects:
| Repository | Description | Stars |
|---|---|---|
 coq-community/coq-art | Coq proof assistant book with exercises and examples | 114 |
 ml4tp/gamepad | A platform that exposes Coq proofs to machine learning algorithms | 72 |
 ejgallego/pycoq | Python bindings for Coq's interactive proof assistant | 50 |
 uwplse/structtact | A Coq library providing structural tactics and utility definitions to simplify proof development in proof assistants. | 21 |
| coq-community/lemma-overloading | A Coq library demonstrating design patterns for automated proof automation and canonical structures | 26 |
| coq-community/chapar | A framework for verifying causal consistency in distributed key-value stores and their clients using the Coq proof assistant | 32 |
 whonore/coqtail | Enables interactive proof development in Vim similar to other proof assistants. | 274 |
 jscoq/jscoq | An online development environment for the proof assistant Coq, allowing users to run and interact with it in their browser. | 518 |
| coq-community/reglang | Provides definitions and verified translations between various representations of regular languages in the Coq proof assistant | 41 |
| coq-community/coq-ext-lib | A collection of reusable Coq definitions and theorems for building software development tools | 129 |
 mit-plv/coqutil | A collection of reusable tools and utilities for working with the Coq proof assistant | 42 |
| coq/vscoq | An extension for Visual Studio Code and VSCodium to support Coq Proof Assistant | 349 |
| ejgallego/coq-lsp | A tool for interactive theorem proving and language support in Coq | 153 |
| coq-community/paramcoq | A Coq plugin providing commands for generating parametricity statements used in data refinement proofs. | 45 |