package coq
Formal proof management system
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.16.0.tar.gz
sha256=36577b55f4a4b1c64682c387de7abea932d0fd42fc0cd5406927dca344f53587
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: 06 Sep 2022
Dependencies (5)
-
zarith
>= "1.11" -
conf-findutils
build -
dune
>= "2.5.1" -
ocamlfind
>= "1.8.1" -
ocaml
>= "4.09.0"
Dev Dependencies
None
Used by (6)
- binary_tree
-
coq-lsp
!= "0.1.6.1+8.17" & < "0.1.7+8.17" | = "0.1.8+8.16" -
coq-serapi
>= "8.16.0+0.16.0" & < "8.17.0+0.17.0" -
coqide
= "8.16.0" - prooftree
-
why3-coq
>= "1.5.1"
Conflicts (2)
On This Page