LEGO projects at Edinburgh

• Rod Burstall, Healf Goguen and Paul Jackson are working on correctness of garbage collection algorithms in collaboration with Harlequin Limited.

• Rod Burstall, Don Sannella and Thomas Schreiber are working on co-development of object-oriented programs in LEGO in collaboration with Darmstadt and Erlangen. The research is partly funded by the DAAD/BC's British-German ARC Programme.

• Healf Goguen and James McKinna are working on subject reduction and type soundness for fragments of SML with references.

• Saif Khan is working on support for object languages in Lego. New commands Terminals and Productions in bnf style rules let you define inductive definitions and first-order algebras in the way of the users choosing.

• Nikos Mylonakis is working on the design of different proof systems for algebraic specifications with the following design criteria: it must be possible to give an adequate encoding of the proposed proof systems in a type-theoretical metalanguage and it must be sound with respect to the semantics of the specification language. After finishing the design, he plans to implement the proof systems using the Lego tool, adding some automatique proof search techniques or decision procedures if necessary.

• Thomas Schreiber is working on co-development of imperative programs and their correctness proofs in a type-theoretic environment. This research is funded by the EU's TMR Programme.

People in the Lego project

Thorsten Altenkirch.
Anthony Bailey.
Stephen Bradley.
Jason Brown.
Rod Burstall.
Pietro Cenciarelli.
Peter Cisek.
Andy Coleman.
Adriana Compagnoni.
Matt Fairtlough.
Healfdene Goguen.
Martin Hofmann.
Claire Jones.
Yoshiki Kinoshita.
Zhaohui Luo.
Savitri Maharaj.
Conor McBride.
James McKinna.
Michael Mendler.
Kevin Mitchell.
Igbinosa Omorogbe.
Christian-Emil Ore.
Randy Pollack.
Thomas Schreiber.
Dilip Sequeira.
Makoto Takeyama.
Paul Taylor.
Judith Underwood
Paul Wand.

Acknowledgement