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

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

Branch: pkgsrc-2007Q4, Version: 8.1pl2, Package name: coq-8.1pl2, Maintainer: richards+netbsd

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/camlp5]

Master sites:

SHA1: 33ab31abffe42559a5c8341b66a0520805337526
RMD160: e45451fdd41b1f979febcfb2c0dbd19a39d09256
Filesize: 2926.938 KB

Version history: (Expand)