PGML is the proposed logical markup language for future versions of Proof General. The basic version legitimizes the present markup scheme which is used by Proof General (based on 8-bit characters). Ideas for PGML are described in the white paper here, but no complete description or DTD is given there. This project is to specify PGML using XML or SGML, and develop some tools for using it. Various tools are desirable, including: (1) a display tool which displays PGML inside Emacs, or converts it to HTML for display by a web browser; (2) a filter or revised version of LEGO which converts its 8-bit markup into PGML, for testing purposes.
Skills: Understanding of markup languages and tools for using and specifying them. Interest in representation of mathematical content. Necessary programming skills.
Proposer: David Aspinall.