Coq proof assistant

I Use This!

Very High Activity

Analyzed about 24 hours ago. based on code collected 1 day ago.

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".

In a Nutshell, Coq proof assistant...

...
has had 42,836 commits made by 351 contributors
representing 492,172 lines of code
...
is mostly written in coq
with a very low number of source code comments
...
has a well established, mature codebase
maintained by a very large development team
with stable Y-O-Y commits
...
took an estimated 134 years of effort (COCOMO model)
starting with its first commit in August, 1999
ending with its most recent commit 1 day ago

Quick Reference

Project Links:

Homepage
Download

Code Locations:

https://github.com/coq/coq

Similar Projects:

Managers:

Become the first manager for Coq proof assistant

Licenses

MIT

Permitted

Commercial Use

Modify

Distribute

Place Warranty

Use Patent Claims

Forbidden

Sub-License

Hold Liable

Required

Distribute Original

Disclose Source

Include Copyright

State Changes

Include License

Include Install Instructions

These details are provided for information only. No information here is legal advice and should not be used as such.

All Licenses

This Project has No vulnerabilities Reported Against it

Did You Know...

...
there are over 3,000 projects on the Open Hub with security vulnerabilities reported against them
...
anyone with an Open Hub account can update a project's tags
...
use of OSS increased in 65% of companies in 2016
...
you can subscribe to e-mail newsletters to receive update from the Open Hub blog