Cette page en Français

peacock feather Pcoq, A graphical user-interface for Coq

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 interactive exercises, and LogiCoq). An alternative solution is to follow this link

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

Yves Bertot
Last modified: Tue Feb 11 11:01:34 MET 2003