Most site members attended the annual workshop in Aussois. Burstall presented a demonstration of his new simplified proof editor, now used in teaching at Edinburgh. McBride discussed further extensions of his work on inversion and unification, and a paper was accepted for publication. it is expected that he will visit the INRIA Rocquencourt site in November to discuss incorporating his work into the Coq theorem prover.
In the spring, Edinburgh hosted Yves Bertot from the INRIA Sophia-Antipolis site, and with Schreiber, Sequeira and Goguen, developed a prrof-by-pointing interface for LEGO, based on existing experience of the Centaur/CtCoq environment. In turn the Edinburgh group have adapted and modularised their Emacs interface to LEGO to run for both LEGO and Coq, incorporating proof-by-pointing and script management. A paper and release versions of the software are in preparation. Schreiber also attended the workshop on User Interfaces for Theorem Provers held at INRIA Sophia-Antipolis in July.
Work on subtyping in Edinburgh and Durham culminated with the Durham workshop on subtyping attended by many of the Edinburgh site, with papers from Goguen and Compaganoni, in addition to Luo, Soloviev, Jones and Yu from Durham. McKinna will take up a teaching appointment in Durham in early 1998, consolidating the TYPES group in Durham.