Edit (March 13, 2018): Pcoq has not been maintained since 2003. Most links on this page are broken. Only the link to the proof-by-pointing paper has been updated.
Pcoq 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 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.
- Java-based
- Pcoq benefits from the combined portability of Ocaml and Java.
Pcoq is developed and maintained in the Lemme team at
INRIA Sophia-Antipolis
. 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
Last updates of this page
- February 11th, 2003.Release of pcoq-1.4
- January 18th, 2002.Release of pcoq-1.3
- May 2nd, 2001. Release of pcoq-1.2