Example project setup for Coq that supports git submodule dependencies
-
Updated
Feb 8, 2020 - Python
Coq is a formal proof management system. It provides a formal language to write
mathematical definitions, executable algorithms and theorems together with an
environment for semi-interactive development of machine-checked proofs. Typical
applications include the certification of properties of programming languages,
the formalization of mathematics and teaching.
Example project setup for Coq that supports git submodule dependencies
REPLICA: REPL Instrumentation for Coq Analysis
An API for interfacing with Coq through Tactician by external agents
A simple theorem prover for Coq.
A parser based on the ALL(*) algorithm, implemented and verified in Coq.
Translates Bluespec SystemVerilog to Kami for use with the coq proof assistant.
Syntax highlighting and Coq interactivity for Sublime Text 3
Tool for suggesting lemma names in Coq verification projects
Jupyter kernel for Coq
Created by Gérard Pierre Huet, Thierry Coquand
Released 1989
Latest release 25 days ago