Coq 8.0 Free Download
Coq 8.0 free downloadDownload
Buy
Coq 8.0 Screenshot Screenshot
    Rate it
Category: Math 
Publisher: The LogiCal project      More titles >>
Last Updated: 5/1/04
Requirements: Not specified
License: Freeware
Operating system: Mac OS X 10.1
Hits: 579
File size: 11.2 MB
Price: Not specified
  • windows free software download
  • apple mac free software download
  • Mobiles, Tablets free apps download

Coq 8.0   Description:

Formal proof management system for mathematics. 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)

Latest Arrivals