May 26, 2018
Theorem prover based on lambda-C
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
- the definition of 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”.
Coq is based on a logical framework called “Calculus of Inductive Constructions” extended by a modular development system for theories.
CoqIde is installed if the x11-toolkits/ocaml-lablgtk2 port is installed.