dc7c8ff64b
- Correct PORTVERSION to match actual source version - Cosmetics PR: ports/73634 Submitted by: Rene Ladan <r.c.ladan@student.tue.nl> (maintainer)
24 lines
795 B
Plaintext
24 lines
795 B
Plaintext
From the website:
|
|
|
|
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.
|
|
|
|
Coq is distributed under the GNU Lesser General Public Licence
|
|
Version 2.1 (LGPL).
|
|
|
|
CoqIde is installed if the x11-toolkits/ocaml-lablgtk2 port is installed.
|
|
|
|
Author: Rene Ladan <r.c.ladan@student.tue.nl>
|
|
WWW: http://coq.inria.fr/
|