Bezem continued the work on a book on Term Rewriting Systems, volume I is scheduled to appear in April 1998. He finished a joint paper with Klop and van Oostrom entitled Diagram Techniques for Confluence (accepted by Information and Computation). Together with students (mainly Hendriks) a start was made with developing an interface between the resolution theorem prover Otter and the proof construction program Coq based on type theory.
Wiedijk did an interesting proof development in ALF during his visit to Gothenburg. His long term goal is to verify the theorem on Jordan curves cutting the real plane in two parts, and to re-edit Landau's Grundlagen with a complete development of the formal proof.