What is Coq 8.0?

Formal proof management system for mathematics.

In depth

A closer look at Coq 8.0

Developed in the LogiCal project, the Coq tool is a formal proof management system: a proof done with Coq is mechanically checked by the machine. In particular, Coq allows:

the definition of interactively evaluated functions or predicates,
to state mathematical theorems and software specifications,
to develop interactively formal proofs of these theorems,
to check these proofs by a small certification "kernel".

Coq is based on a logical framework called "Calculus of Inductive Constructions" extended by a modular development system for theories.

Coq also includes

a mecanism for automatic generation of certified programs from proofs of their specifications
a graphical user interface based on gtk (CoqIde)
a documentation tool (coqdoc)
dependecy and makefile generation tools for Coq (coq_makefile and coqdep)
a preprocessor for TeX files that include Coq commands (coq-tex)

Coq is written in the Objective Caml language and uses the Camlp4 Pre-processor-pretty-printer for Objective Caml. Coq is distributed under the GNU Lesser General Public Licence Version 2.1 (LGPL). It is currently available for Unix (including Mac OS X)

Verdict

Should you download Coq 8.0?

Coq 8.0 runs on Mac OS X 10.1 and is available under the Freeware license — the installer is 11.2 MB. We’ve catalogued it under Math.

Verified clean. Every Coq 8.0 build on SoftLookup is scanned for viruses, spyware, adware, trojans and backdoors. We re-test on every update.

Coq 8.0 specifications

Category: Math
Publisher: The LogiCal project
Last updated: Apr 1, 2026
License: Freeware
Operating system: Mac OS X 10.1
File size: 11.2 MB
Price: Free
Page views: 435

Help fellow users decide. Share your experience with Coq 8.0.

Coq 8.0

What is Coq 8.0?

A closer look at Coq 8.0

Should you download Coq 8.0?

Coq 8.0 specifications

Leave a comment