PGIP is a protocol for interactive proof to be used in the next version of Proof General. It is based around the present protocol, but implemented with a standard collection of messages rather than different messages for different proof assistants. An outline of PGIP is given in the white paper. A first implementation of PGIP will consist of (1) a filter (or modification of the output routines) for an existing proof assistant, which could be implemented in perl or some other language; and (2) a new backend for Proof General in Emacs, which configures it for PGIP.
Skills: Interest in interactive proof and basic understanding of interaction mechanisms with at least one of LEGO, Coq, Isabelle. Programmming in Emacs Lisp.
Proposer: David Aspinall.