Cette page en Français

peacock feather Pcoq, A graphical user-interface for Coq

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 developped 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

  • January 18th, 2002.Release of pcoq-1.3
  • May 2nd, 2001. Release of pcoq-1.2

Yves Bertot
Last modified: Tue Feb 11 14:57:39 MET 2003