diff options
| author | David Aspinall | 2000-05-09 10:31:34 +0000 |
|---|---|---|
| committer | David Aspinall | 2000-05-09 10:31:34 +0000 |
| commit | 6039328a88ff67d4bca86dead469b10cb1aba377 (patch) | |
| tree | 0f39a4ef6be79bb407ff8e9cd032c2c5fd4ea89d /html/projects/xmlpgip.html | |
| parent | 22a37c6259afd7eab99afcc18641dfa0c294c1bd (diff) | |
New project (unlinked yet)
Diffstat (limited to 'html/projects/xmlpgip.html')
| -rw-r--r-- | html/projects/xmlpgip.html | 40 |
1 files changed, 40 insertions, 0 deletions
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 @@ +<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> +<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN"> +<html> + <head> + <title></title> + </head> + + <body> + <h1></h1> + + + + <hr> + <address><a href="mailto:da@dcs.ed.ac.uk">David Aspinall</a></address> +<!-- Created: Tue Apr 25 18:11:06 BST 2000 --> +<!-- hhmts start --> +Last modified: Tue Apr 25 18:22:01 BST 2000 +<!-- hhmts end --> + </body> +</html> |