
Pcoq provides a working environment for the
Coq theorem prover.
It has been developed following a general
approach
for building userinterfaces 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 graphical 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, new notations can easily be added,
 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.
 Javabased

Pcoq benefits from the combined portability of
Ocaml and
Java.
Pcoq is developed and maintained in the Lemme team at
INRIA SophiaAntipolis
. This group is interested in many aspects of using
the Coq system. For instance, we have also collaborated
with Xiao Gang from University of Nice to make Coq
available on the web through his
interactive mathematics server. (follow the links
interactive exercises, and LogiCoq). An
alternative solution is to follow
this link
Last updates of this page
 February 11th, 2003.Release of pcoq1.4
 January 18th, 2002.Release of pcoq1.3
 May 2nd, 2001. Release of pcoq1.2
