From b37bf74fc2d6309a5ae3dc6b55e8488409976775 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 29 Feb 2000 06:19:39 +0000
Subject: New projects directory.

---
 html/projects/pgip.html | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)
 create mode 100644 html/projects/pgip.html

(limited to 'html/projects/pgip.html')

diff --git a/html/projects/pgip.html b/html/projects/pgip.html
new file mode 100644
index 00000000..22cc654b
--- /dev/null
+++ b/html/projects/pgip.html
@@ -0,0 +1,21 @@
+<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
+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>
-- 
cgit v1.2.3