INRIA Sophia Antipolis
Cette page en Franšais
Ctcoq is now replaced by a new system, called
What is CtCoq
CtCoq provides a working environment for the
theorem prover. It
has been developed following a general approach for
building user-interfaces for theorem provers. It has the following
- 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
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 firstname.lastname@example.org.
CtCoq profits from work done on programming environments, in particular
system, developed in the
INRIA Sophia Antipolis.
Yves Bertot / INRIA Sophia Antipolis / Yves.Bertot@inria.fr