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

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

Branch: pkgsrc-2010Q1, Version: 8.2pl1, Package name: coq-8.2pl1, 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: 4aed3302adc2edbaa5d97984512c1c13014bd649
RMD160: dd5758a94bb3de49967cec76baa33eb5169659ce
Filesize: 3516.23 KB

Version history: (Expand)