blob: 46cdd96023556622a47b4e5ab036f05e292d3ddd (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
<h2>Specification and tools for PGML</h2>
<p>
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
<a href="/home/da/drafts/#white">here</a>, 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.
</p>
<p>
<b>Skills:</b>
Understanding of markup languages and tools for using and specifying them.
Interest in representation of mathematical content.
Necessary programming skills.
</p><p>
<b>Proposer:</b>
<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
</p>
|
