Next: University of Helsinki
Up: Progress Report
Previous: University of Durham
University of Edinburgh
At Edinburgh work has continued on application of type theory to
proof. Goguen and Burstall working with Brooksby of Harlequin
produced a proof in Coq for a concurrent garbage collector. Kleymann
wrote a thesis on a proof of soundness and completeness of Hoare
Logics, and McBride wrote one on dependent types for developing
functional programs. Burstall continued to develop the ProveEasy tool
for teaching logic. Kleymann and Aspinall released Proof General, an
emacs interface for theorem provers (Coq, Lego, Isabelle).
Next: University of Helsinki
Up: Progress Report
Previous: University of Durham