coq - The Coq Proof Assistant
| Website: | http://coq.inria.fr/ |
|---|---|
| License: | LGPLv2 |
- Description:
Coq is a Proof Assistant for a Logical Framework known as the Calculus of Inductive Constructions. It allows the interactive construction of formal proofs, and also the manipulation of functional programs consistently with their specifications.
Packages
| coq-8.3pl2-1m.mo8.x86_64 [37.6 MiB] |
Changelog
by NARITA Koichi (2011-12-19):
- (8.3pl2-1m) - update to 8.3pl2 |