New projects directory.

1 files changed, 32 insertions, 0 deletions

diff --git a/html/projects/thybrowse.html b/html/projects/thybrowse.html
new file mode 100644
index 00000000..bb081fc0
--- /dev/null
+++ b/html/projects/thybrowse.html
@@ -0,0 +1,32 @@
+<h2>A Generic Theory Browser</h2>
+<p>
+Proof General has very limited mechanisms for helping the user find
+theorems and definitions during a proof.  It has notion of displaying
+a "current context" for a proof, and configuration with a proof
+engine command for searching for theorems.  It would be useful to
+extend these facilities with a <i>theory browser</i> for investigating
+the theories currently defined in a running proof assistant.  This
+involves designing a small protocol to communicate with the proof
+assistant and a generic way of displaying theories which have
+different aspects from system to system.  A way which would
+fit in well with Emacs would be to use a <tt>dired</tt>-like
+buffer.
+</p>
+<p>
+An alternative version of this project would be to write a standalone
+theory browser which uses an extension of the forthcoming Proof
+General standardized protocol for interaction (see white paper <a
+href="/home/da/drafts/#white">here</a>).  This could be implemented in
+Java, or in a functional language, Perl, C or C++, so long as a nice
+toolkit is chosen (Qt or GTK).
+</p>
+<p>
+<b>Skills:</b>
+Interface programming skills.
+Basic understanding of what theories are for several different proof
+assistants.
+</p><p>
+<b>Proposer:</b>
+<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
+</p>
+