Bug 72718 - [NEW PORT] math/coq: Theorem prover based on lambda-C
Summary: [NEW PORT] math/coq: Theorem prover based on lambda-C
Status: Closed FIXED
Alias: None
Product: Ports & Packages
Classification: Unclassified
Component: Individual Port(s) (show other bugs)
Version: Latest
Hardware: Any Any
: Normal Affects Only Me
Assignee: freebsd-ports-bugs (Nobody)
URL:
Keywords:
Depends on:
Blocks:
 
Reported: 2004-10-15 01:00 UTC by Rene Ladan
Modified: 2004-10-16 01:57 UTC (History)
0 users

See Also:

Attachments
coq-8.0.shar (21.16 KB, text/plain)
2004-10-15 01:00 UTC, Rene Ladan 		no flags Details
View All Add an attachment (proposed patch, testcase, etc.)

Note You need to log in before you can comment on or make changes to this bug.
Description Rene Ladan 2004-10-15 01:00:51 UTC 
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 not yet available in this port.

Author: Rene Ladan <r.c.ladan@student.tue.nl>
WWW:    http://coq.inria.fr/

Generated with FreeBSD Port Tools 0.63
Comment 1 Pav Lucistnik freebsd_committer freebsd_triage 2004-10-16 01:57:22 UTC 
State Changed
From-To: open->closed

New port added, thank you!