Developer website:
The LogiCal project
Developed in the LogiCal project, the Coq tool is a formal proof management system: a proof done with Coq is mechanically checked by the machine. In particular, Coq allows:
More...
- the definition of interactively evaluated functions or predicates,
- to state mathematical theorems and software specifications,
- to develop interactively formal proofs of these theorems,
- to check these proofs by a small certification "kernel".
More...
Requirements
Mac OS X 10.1 or laterSimilar Software
Suggest other similar software
Coq User Discussion
Ratings
Details