              INRIA Sophia Antipolis
         CtCoq distribution

Cette page en Français

Ctcoq is now replaced by a new system, called pcoq

What is CtCoq

CtCoq provides a working environment for the Coq theorem prover. It has been developed following a general approach for building user-interfaces for theorem provers. It has the following characteristics:

graphical interface:: Multiple fonts and colors are used to display formulas and commands,
separation between the interface and the prover:: The X interface and Coq run as two separate processes. Users may choose which machine to run Coq on in their network of workstations.
structured editing and presentation mechanisms:: The environment provides ways to edit structurally formulas and commands, whole sub-expressions can be shrunk in one click of the mouse and new notations can easily be added,
menu directed editing:: The environment provides menus for editing new commands and formulas, these menus can easily be extended to incorporate the user's favorite command or formula patterns.
proof by pointing:: The environment uses the structure of logical formulas to help systematically the user direct the proof by simple clicks of the mouse.

A precise description of Ctcoq's architecture and main features can be found in an INRIA report. To know more about CtCoq, you may also want to have a look at its on-line documentation.

How to get CtCoq

The CtCoq interface runs with Coq version 6.2.3 exclusively. You can get the CtCoq system or you may just be interested in some related papers or documentation.
For more information mail to ctcoq-request@sophia.inria.fr.

General Info

CtCoq profits from work done on programming environments, in particular the Centaur system, developed in the Croap group at INRIA Sophia Antipolis.

Yves Bertot / INRIA Sophia Antipolis / Yves.Bertot@inria.fr