{\rtf1\mac\ansicpg10000\cocoartf100
{\fonttbl\f0\fswiss\fcharset77 Helvetica;}
{\colortbl;\red255\green255\blue255;}
\margl1440\margr1440\vieww9000\viewh9000\viewkind0
\pard\tx1440\tx2880\tx4320\tx5760\tx7200\ql\qnatural

\f0\fs24 \cf0 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 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 mechanism for automatic generation of certified programs\
  from proofs of their specifications\
- a graphical user interface based on gtk (CoqIde)\
- a documentation tool (coqdoc)\
- dependency 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.\
}