./lang/coq, Theorem prover which extracts programs from proofs

[ CVSweb ] [ Homepage ] [ RSS ] [ Required by ] [ Add to tracker ]

Branch: pkgsrc-2013Q1, Version: 8.4pl1nb3, Package name: coq-8.4pl1nb3, Maintainer: jaapb

From http://coq.inria.fr/doc/tutorial.html:

Coq is a Proof Assistant for a Logical Framework known as the
Calculus of Inductive Constructions. It allows the interactive
construction of formal proofs, and also the manipulation of
functional programs consistently with their specifications.


Required to run:
[lang/ocaml]

Required to build:
[pkgtools/x11-links]

Package options: coqide

Master sites:

SHA1: 23d403dbe9e410a99c584d0210dc527950051679
RMD160: fa472852de474ed5b83ddd4bd5a303f32b5dba94
Filesize: 4042.781 KB

Version history: (Expand)