package coq

  1. Overview
  2. Docs
Formal proof management system

Install

Dune Dependency

Authors

Maintainers

Sources

V8.10.1.tar.gz
sha512=5c6a20e283c351a4b0ecdb393fb77cfc9b72b474453c99c95f52a70da47dd72fff7229c2ef92d61aadade8f2ed6e03c1a7740d0fa2fcc87ea72659f95eceb2dc

Description

The Coq proof assistant 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 (e.g., the CompCert compiler certification project and the Bedrock verified low-level programming library), the formalization of mathematics (e.g., the full formalization of the Feit-Thompson theorem and homotopy type theory) and teaching.

Published: 28 Oct 2019

Dependencies (4)

  1. conf-findutils build
  2. num
  3. ocamlfind build
  4. ocaml >= "4.05.0" & < "4.10"

Dev Dependencies

None

Used by (4)

  1. coq-serapi >= "8.10.0+0.7.0" & < "8.11.0+0.11.0"
  2. coqide = "8.10.1"
  3. why = "2.32" | = "2.34"
  4. why3-coq >= "1.3.0" & < "1.7.0"

Conflicts

None

OCaml

Innovation. Community. Security.