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

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

Branch: pkgsrc-2012Q1, Version: 8.3pl1nb8, Package name: coq-8.3pl1nb8, 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.

Master sites:

SHA1: 3fae9fa2fd6f39c9fb3c0b67fcd5e71f1e7a5f9f
RMD160: 687983bcaca723299b6ea902a1e1b07338209d55
Filesize: 3668.907 KB

Version history: (Expand)