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".
released on 1 September 2007
|License||Verified by||Verified on||Notes|
|LGPLv2.1||Deborah Nicholson||25 June 2008|
Leaders and contributors
Resources and communication
This entry (in part or in whole) was last reviewed on 25 June 2008.