From b9caaa8e4b66817dbc66d0e79b567b3285869fea Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Sat, 7 Feb 2004 19:31:13 +0000 Subject: Deleted file --- html/projects/xmlpgip.html | 40 ---------------------------------------- 1 file changed, 40 deletions(-) delete mode 100644 html/projects/xmlpgip.html (limited to 'html/projects/xmlpgip.html') diff --git a/html/projects/xmlpgip.html b/html/projects/xmlpgip.html deleted file mode 100644 index 30828a97..00000000 --- a/html/projects/xmlpgip.html +++ /dev/null @@ -1,40 +0,0 @@ -

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