A Web-based Proof Replayer for Proof General

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 displaying the results. Ideally, the ideas for new standard protocols for Proof General in the white paper would be followed.

Skills: Strong web programming skills using scripting languages, dynamic HTML, etc.

Proposer: David Aspinall.