From 6039328a88ff67d4bca86dead469b10cb1aba377 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 9 May 2000 10:31:34 +0000 Subject: New project (unlinked yet) --- html/projects/xmlpgip.html | 40 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) create mode 100644 html/projects/xmlpgip.html (limited to 'html') diff --git a/html/projects/xmlpgip.html b/html/projects/xmlpgip.html new file mode 100644 index 00000000..30828a97 --- /dev/null +++ b/html/projects/xmlpgip.html @@ -0,0 +1,40 @@ +

A New Protocol for Interactive Proof in Proof General

+

+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 white paper. 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. +

+

+Skills: +Interest in interactive proof and basic understanding +of interaction mechanisms with at least one of +LEGO, Coq, Isabelle. Programmming in Emacs Lisp. +

+Proposer: +David Aspinall. +

+ + + + + + + +

+ + + +
+
David Aspinall
+ + +Last modified: Tue Apr 25 18:22:01 BST 2000 + + + -- cgit v1.2.3