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

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

Branch: pkgsrc-2011Q3, Version: 8.3pl1nb1, Package name: coq-8.3pl1nb1, 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: 3fae9fa2fd6f39c9fb3c0b67fcd5e71f1e7a5f9f
RMD160: 687983bcaca723299b6ea902a1e1b07338209d55
Filesize: 3668.907 KB

Version history: (Expand)