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

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

Branch: pkgsrc-2007Q3, Version: 8.1nb1, Package name: coq-8.1nb1, 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 build:
[lang/ocaml] [devel/gmake]

Master sites:

SHA1: 151aca5b7c919eeb39ba3c6fecec836b7953b206
RMD160: 548d2e25e7813567252f9b176f318619a780d729
Filesize: 2907.365 KB

Version history: (Expand)