The Group at Durham has organised the TYPES WG Workshop on "Subtyping, inheritance and modular development of proofs" (see web page http://www.dur.ac.uk/ dcs3apj/cs-types/).
Zhaohui Luo, Sergei Soloviev, and Alex Jones have been studying Coercive Subtyping for type theory, its meta-theory and applications [1][2].
Shenwei Yu has implemented a model checker, LegoMC, for the Lego system and studied its applications in verification of concurrent programs, including infinite-state problems as well as finite-state problems [3].
The reseach project on developing and implementing a mathematical vernacular (Zhaohui Luo and Paul Callaghan) [4], and a related research on proof explanation (Maria Fox) are in progress.
The Lego system has been used in applications to reverse-engineering concurrent programs (Eddy Younger) [6] and formal reasoning about AI planning theories (Maria Fox and Derek Long) [5].
References
[1] Z. Luo. Coercive subtyping in type theory. Proc. of CSL'96, the 1996 Annual Conference of the European Association for Computer Science Logic, Utrecht. LNCS 1258, 1997.
[2] A. Jones, Z. Luo, and S. Soloviev. Some algorithmic and proof-theoretical aspects of coercive subtyping. Proc. of TYPES'96, Accepted and to appear in LNCS.
[3] S. Yu and Z. Luo. Implementing a model checker for Lego. Proc. of the 4th Inter Symp. of Formal Methods Europe, FME'97: Industrial Applications and Strengthened Foundations of Formal Methods, Graz, Austria. LNCS 1313, 1997.
[4] Z. Luo and P. Callaghan. Linguistic categories in mathematical vernacular and their type-theoretic semantics (extended abstract). Logical Aspects of Computational Linguistics 97 (LACL'97), 1997.
[5] M. Fox and D. Long. Formalising non-linear lanning. Manuscript, 1997.
[6] E.J. Younger, K.H. Bennett, and Z. Luo. A formal transformation and refinement method for re-engineering concurrent programs. Proc. of IEEE ICSM'97, Bari, Italy, 1997.