|
 |
bbf312f |
# coq
|
|
|
bbf312f |
|
|
|
bbf312f |
Coq is a formal proof management system. It provides a formal language to
|
|
|
bbf312f |
write mathematical definitions, executable algorithms and theorems together
|
|
|
bbf312f |
with an environment for semi-interactive development of machine-checked
|
|
|
bbf312f |
proofs. Typical applications include the
|
|
|
bbf312f |
[certification of properties of programming languages](https://coq.inria.fr/cocorico/List%20of%20Coq%20PL%20Projects)
|
|
|
bbf312f |
(e.g. the [CompCert])(https://compcert.org/) compiler certification project,
|
|
|
bbf312f |
the [Verified Software Toolchain](https://vst.cs.princeton.edu/) for
|
|
|
bbf312f |
verification of C programs, or the [Iris](https://iris-project.org/) framework
|
|
|
bbf312f |
for concurrent separation logic), the
|
|
|
bbf312f |
[formalization of mathematics](https://coq.inria.fr/cocorico/List%20of%20Coq%20Math%20Projects)
|
|
|
bbf312f |
(e.g. the full formalization of the
|
|
|
bbf312f |
[Feit-Thompson theorem](https://hal.inria.fr/hal-00816699), or
|
|
|
bbf312f |
[homotopy type theory](https://homotopytypetheory.org/coq/)), and
|
|
|
bbf312f |
[teaching](https://github.com/coq/coq/wiki/CoqInTheClassroom).
|
|
|
bbf312f |
|
|
|
bbf312f |
The [Reference Manual](https://coq.inria.fr/distrib/current/refman/) and the
|
|
|
bbf312f |
[Standard Library documentation](https://coq.inria.fr/distrib/current/stdlib/)
|
|
|
bbf312f |
are the primary documentation for Coq. However, to learn about Coq, we
|
|
|
bbf312f |
recommend starting with a tutorial or book, such as those listed on the
|
|
|
bbf312f |
[documentation page](https://coq.inria.fr/documentation).
|