[X] I have searched all issues/PRs to ensure it has not already been reported or fixed.
Criteria
[X] Reasonably well-known and widely used (e.g. if it's a GitHub project, it should have at least 100 stars and/or 50 forks)
[X] English interface (or at least English documentation)
[X] Latest stable version
[X] Full version (i.e. not a trial version)
[X] Fairly standard install (e.g. uses a version-specific download URL, no elaborate pre/post install scripts)
Name
coq
Description
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 (e.g. the CompCert compiler certification project, the Verified Software Toolchain for verification of C programs, or the Iris framework for concurrent separation logic), the formalization of mathematics (e.g. the full formalization of the Feit-Thompson theorem, or homotopy type theory), and teaching.
aliesbelik
commented
7 months ago
Prerequisites
Criteria
Name
coq
Description
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 (e.g. the CompCert compiler certification project, the Verified Software Toolchain for verification of C programs, or the Iris framework for concurrent separation logic), the formalization of mathematics (e.g. the full formalization of the Feit-Thompson theorem, or homotopy type theory), and teaching.
Homepage
https://coq.inria.fr/
Download Link(s)
https://github.com/coq/platform/releases
Some Indication of Popularity/Repute
Official GitHub repository has 43 forks and 178 stars ➡️ https://github.com/coq/platform