blob: 2557addcc410b7c9a2a40803247ad77b3a61a3b6 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
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.
WWW: http://coq.inria.fr/
|
