blob: 073edd0664d1c31ed29720a5b3613df5810021be (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
<h2>A New Protocol for Interactive Proof in Proof General</h2>
<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
and an experimental DTD
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>
|
