Docker images of the Coq proof assistant (see also: https://github.com/coq-community/docker-coq-action) [maintainers=@erikmd]
-
Updated
May 13, 2025 - Shell
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.
Docker images of the Coq proof assistant (see also: https://github.com/coq-community/docker-coq-action) [maintainers=@erikmd]
Translating the Plutus standard library to Coq
Docker images of the Coq proof assistant with compcert and VST pre-installed
🐓 Coq plugin for ASDF version manager.
Bash script for simple generation of Coq project metadata files
A regression proof selection tool for the Coq proof assistant
Created by Gérard Pierre Huet, Thierry Coquand
Released 1989