Project Summary
Coq is a formal proof management system: a proof done with Coq is mechanically checked by the machine. In particular, Coq allows:
* to define functions or predicates,
* to state mathematical theorems and software specifications,
* to develop interactively formal proofs of these theorems,
* to check these proofs by a relatively small certification "kernel".
Quick Reference
- Project Links:
-
Homepage
Download
- Code Locations:
-
svn://scm.gforge.inria.fr/svn/co...
- Licenses:
- LGPL
- Similar Projects:
-
- Managers:
- Become the first manager for Coq proof assistant
In a Nutshell, Coq proof assistant...
- ...
- ...
-
...
has a well established, mature codebase
maintained by a large development team
with stable Y-O-Y commits -
...
took an estimated 93 years of effort (COCOMO model)
starting with its first commit in August, 1999
ending with its most recent commit 4 days ago
Activity
30 Day Summary May 18 2013 — Jun 17 2013
|
12 Month Summary Jun 17 2012 — Jun 17 2013
|
Community
Copyright
©
2013
Black Duck Software, Inc.
and its contributors, Some Rights Reserved. Unless otherwise marked, this work is licensed under a
Creative Commons Attribution 3.0 Unported License
. Ohloh
®
and the Ohloh logo are trademarks of
Black Duck Software, Inc.
in the United States and/or other jurisdictions. All other trademarks are the property of their respective holders.