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

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

Branch: pkgsrc-2014Q1, Version: 8.4pl2nb12, Package name: coq-8.4pl2nb12, Maintainer: jaapb

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.



Package options: coqide

Master sites:

SHA1: adcef430b8e27663e8ea075e646112f7d4d51fa6
RMD160: 4860eaff4c8f0a235d3fcf162199eaa5fe1db2da
Filesize: 4047.961 KB

Version history: (Expand)