path: root/html/projects.phtml

<?php  
  require('functions.php3');
  small_header("Proof General Project Proposals"); 
  ?>

<p>
Here are some proposals for projects connected to Proof General.
</p>
<p>
The projects are designed as fairly self-contained contributions,
involving code development and possibly a portion of supporting
research.  They would be ideal projects for interested students
or researchers.
</p>

<ul>
<li><b>Proof-by-pointing support for Coq</b>
<p>
Coq already has sophisticated notions of proof-by-pointing,
and old work on support for Proof General may be helpful.  
We want to integrate with the latest version of Coq's
proof-by-pointing, possibly improving Proof General's
support along the way.
</p>
<p>
<b>Skills:</b>
 Some understanding of Coq implementation, co-operation with
 the Coq developers to get any Coq modifications (if any) incorporated.
 Minimal Emacs Lisp knowledge. 
</p><p>
<b>Proposer:</b>
<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
</p>

<li><b>Proof-by-pointing support for Isabelle</b>
<p>
Isabelle has a sophisticated concrete syntax mechanism which makes it
difficult to add annotations to connect the displayed output back to
the internal abstract syntax.  This issue needs to be solved to
support proof-by-pointing (and other features) in Isabelle.
A 
<a href="http://www.informatik.uni-bremen.de/~bu/isa_contrib/isabelle.html">
patch by Burkhart Wolff</a> 
providing term structure annotations for a previous release of
Isabelle may be useful here.  To implement proof-by-pointing itself,
tactics using the gesture information must be written.
</p>
<p>
<b>Skills:</b>
 Some understanding of Isabelle implementation, 
 co-operation with the Isabelle developers to get
 Isabelle modifications incorporated.
 Skill in writing Isabelle tactics.
 Minimal Emacs Lisp knowledge.
</p><p>
<b>Proposer:</b>
<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
</p>
</li>

<li><b>Integrating block-structured development and outline mode</b>
<p>
Emacs already provides powerful outline facilities (cf. the
outl-minor-mode setup for the well-known auc-tex package).  
Similarly, proof systems such as Isabelle/Isar are inherently based on
block-structured proof texts, with compositional proof checking.
</p><p>
But Proof General currently offers a mostly linear model of
incremental script management.  The aim of this project is to extend that
model to a hierarchic one: e.g. sub-proofs could be suppressed in the
presentation, or even temporarily suspended (to achieve top-down
development).
</p><p>
Outline support would be useful for the large scale structure of formal
developments as well, e.g. support the basic arrangement into logical
section (cf. Coq), or even just traditional layout-based ones (cf. LaTeX).
</p>
<p>
<b>Skills:</b>
Some understanding of the workings of Emacs outline mode and Proof
General script management.  Good portion of Emacs lisp knowledge.
</p><p>
<b>Proposer:</b>
<a href="http://www.in.tum.de/~wenzelm/">Markus Wenzel</a>.
</p>
</li>


<li><b>Multiplexed Modes for Emacs</b>
<p>
Emacs has a mechanism for customizing the editing behaviour of buffers
based on their <i>major mode</i>.  A buffer can only have one major
mode, but in literate styles of programming and proving we want to mix
program text with documentation in a single file.  A way of
multiplexing major modes is needed, so that different regions of a
buffer can be edited in different modes.  One approach may be to use
"views" onto untangled buffers, although it isn't clear how search and
replace, etc, should behave in this case.  
</p><p>
Emacs hackers may already have worked on this problem and solved it
sufficiently well (does anybody know?), in which case this project
might degenerate into applying the work for Coq and Isabelle/Isar, as
a feasibility demonstration.
</p><p>
<b>Skills:</b>
A passion for Emacs and Emacs Lisp.
</p><p>
<b>Proposer:</b>
<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
</p>
</li>

<li><b>Script General</b>
<p>
Proof General is based around a core system of script management
for proof scripts.  But the idea of script management is not
restricted to proof assistants, it makes sense for many interactive
scripting languages.  It deserves to be better known and used.
A worthwhile project would be to rewrite the core script management
features of Proof General so that they could work for arbitrary
interactive scripting languages, and instantiate to Proof General as
well as languages such as ML, Haskell, LISP, Scheme, Python, and
even Emacs Lisp itself.
</p>
<p>
An alternative version of this project is to implement a 
generic basis for script management which does <i>not</i> depend on 
Emacs, but uses a similar protocol to communicate with other
text editors or display widgets.  This could be implemented in
SML, OCaml, Java, C++, or any other suitable language.
<p>
<b>Skills:</b>
Proficient Emacs Lisp (or other programming language), 
knowledge of scripting languages desirable.
</p><p>
<b>Proposer:</b>
<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
</p>
</li>

<!-- <li><b> </b> -->
<!-- <p> -->
<!-- </p> -->
<!-- <p> -->
<!-- <b>Skills:</b> -->
<!-- </p><p> -->
<!-- <b>Proposer:</b> -->
<!-- <a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>. -->
<!-- </p> -->
<!-- </li> -->

</ul>



<p>
If you are interested in working on any of these projects,
feel free to discuss with the project proposer or on the 
<?php link_root("devel#develmail","developer's mailing list") ?>.
</p>
<p>
Note: the proposer of the project is just that; he or she does not
guarantee to be available for formal supervision or intensive help
with the project.  But it may be possible to find somebody else
to do that.  Contact the project proposer first for more details.
</p>

<p>
If you would like to use any of these ideas as a formal project
proposal for students at your institution, please feel free
but do <?php hlink("feedback.phtml","let us know ","Feedback form")?>
if some work is begun, to help coordinate effort.
</p>

<p>
If you would like to submit a project proposal
for an improvement or extension of Proof General,
please send an email or write a description on the 
<?php hlink("feedback.phtml","web feedback form","Feedback form")?>.
Projects should be significant contributions rather than
incremental improvements (although we welcome the suggestion of those
too).
</p>


<?php
   click_to_go_back();
   footer();
?>