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

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

Branch: pkgsrc-2015Q1, Version: 8.4pl4nb3, Package name: coq-8.4pl4nb3, 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.


Required to run:
[lang/camlp5] [lang/ocaml]


Package options: coqide

Master sites:

SHA1: 4dfc3a1ae65f5c480ddc4387d21549a526183e00
RMD160: 19e3fe905f5db09710b1f862f21e9b57c28f9704
Filesize: 3972.026 KB

Version history: (Expand)