blob: 8d418d5b4ecbf6b43fd669b62c1409cf68a3344f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
|
{\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.\
}
|
