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). The ideas for PGML are described in the white paper here, and an experimental DTD is given there. This project is to refine the specification of PGML, and develop some tools for using it. Various tools are desirable, including: (1) translation tools which convert PGML to various other formats, such as HTML and LaTeX. (2) a display tool which displays PGML inside Emacs, or converts it to HTML for display by a web browser; (3) a filter or revised version of LEGO which converts its 8-bit markup into PGML, for testing purposes. We need the last tool for other proof assistants too.
Skills: Understanding of markup languages and tools for using and specifying them. Interest in representation of mathematical content. Necessary programming skills.
Proposer: David Aspinall.