Current system developments at Edinburgh include dependent pattern-matching and a generic Emacs interface for proof systems. We plan to release these within the next 12 months.
In addition, an active research group of Computer-Assisted Reasoning at the University of Durham, whose members include two former members of the LEGO group, Zhaohui Luo and James McKinna, are continuing the research into theory, practice and applications of type theory based theorem proving, using the latest release of LEGO, as well as other systems.
Last updated on 9 June 1998 by <lego@dcs.ed.ac.uk>