blob: 4ec8f14881134c69458621a2f0b0dc2cdd7a4c34 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
{\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 Developped in the INRIA LogiCal project, The Coq tool is a proof\
assistant which:\
\
- allows to handle calculus assertions,\
- allows to check mechanically proofs of these assertions,\
- helps to find formal proofs,\
- extracts a certified program from the constructive proof of its formal specification,\
\
Coq is written in the Objective Caml language and uses the Camlp4\
Pre-processor-pretty-printer for Objective Caml.\
}
|
