Added some more projects

1 files changed, 77 insertions, 3 deletions

diff --git a/html/projects.phtml b/html/projects.phtml
index 022aa052..a4000ab6 100644
--- a/html/projects.phtml
+++ b/html/projects.phtml
@@ -155,9 +155,10 @@ buffer.
 <p>
 An alternative version of this project would be to write a standalone
 theory browser which uses an extension of the forthcoming Proof
-General standardized protocol for interaction.  This could be
-implemented in Java, or in a functional language, Perl, C or C++, so
-long as a nice toolkit is chosen (Qt or GTK).
+General standardized protocol for interaction (see white paper <a
+href="/home/da/drafts/#white">here</a>).  This could be implemented in
+Java, or in a functional language, Perl, C or C++, so long as a nice
+toolkit is chosen (Qt or GTK).
 </p>
 <p>
 <b>Skills:</b>
@@ -170,6 +171,79 @@ assistants.
 </p>
 </li>
 
+<li><b>Specification and tools for PGML</b>
+<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).
+Ideas for PGML are described in the white paper 
+<a href="/home/da/drafts/#white">here</a>, 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.
+</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> 
+</li> 
+
+
+<li><b>A New Protocol for Interactive Proof in Proof General</b>
+<p>
+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 <a href="/home/da/drafts/#white">white paper</a>.  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.
+</p>
+<p>
+<b>Skills:</b>
+Interest in interactive proof and basic understanding
+of interaction mechanisms with at least one of 
+LEGO, Coq, Isabelle.   Programmming in Emacs Lisp.
+</p><p>
+<b>Proposer:</b>
+<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
+</p>
+</li>
+
+<li><b>A Web-based Proof Replayer for Proof General</b>
+<p>
+One of the nice features of Proof General is that it is very easy to
+replay existing proofs, by mouse clicks alone.  No low-level
+understanding of a proof assistant is needed to step through proofs.
+We would like to have a web-based version of Proof General which
+allowed for this proof replay (at least), perhaps running a proof
+assistant remotely.  The main aspect is to implement an engine for
+script management (colouring of lines of files), displaying in a web
+browser, sending lines to a proof assistant process, and display the
+results.  Ideally, the ideas for new standard protocols for Proof
+General in the <a href="/home/da/drafts/#white">white paper</a> would
+be followed.
+</p>
+<p>
+<b>Skills:</b>
+Strong web programming skills using scripting languages,
+dynamic HTML, etc.
+</p><p>
+<b>Proposer:</b>
+<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
+</p>
+</li>
+
 <!-- <li><b> </b> -->
 <!-- <p> -->
 <!-- </p> -->