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

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

Branch: pkgsrc-2009Q2, Version: 8.1pl3nb1, Package name: coq-8.1pl3nb1, 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]

Required to build:
[devel/gmake] [lang/ocaml]

Master sites:

SHA1: c06141891c2a793ff6b4bc1f106d9477b3a9a52e
RMD160: f8f4749e1014cb47a83915550713cf9ce1992e34
Filesize: 2933.196 KB

Version history: (Expand)