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.2-7m.mo6.x86_64 [35.8 MiB] |
Changelog
by TABUCHI Takaaki (2009-07-30):
- (8.2-7m) - rebuild against emacs 23.1 |