His research interests include functional languages (development of HOPE and Standard ML), algebraic specification languages (CLEAR, ASL, Extended ML, CASL), mechanised reasoning, foundations for algebraic specification and formal software development including correctness of modular systems, and applying these foundations to the practical development of modular software systems from specifications. His recent research has focused on security and static analysis with a specific emphasis on resource certification for mobile code. He is founder and CTO of Contemplate Ltd, a spin-out technology company that is developing tools for programmers to improve the quality of software products.
He has published a research monograph and more than 60 papers in journals and international conferences and has held a series of grants since 1985 for research projects in the area of verification and formal development of programs. He has served on the programme committee of 45 international conferences and was programme chair of ESOP'94 and track B of ICALP 2004, and general chair of CAAP/ESOP/CC'94 and ETAPS 2005 in Edinburgh. He is editor-in-chief of the journal Theoretical Computer Science (responsible for part B: Logic, Semantics and Theory of Programming) and an editor of Electronic Notes in Theoretical Computer Science. He served as chairman of the steering committee of the ETAPS conference series from its inception in 1995 until 2001, then as treasurer until 2008, then as representative of the European Association for Theoretical Computer Science. He served as Vice President of EATCS from 2008 until 2012. Sixteen Ph.D. theses have been completed under his supervision; two of these won the British Computer Society's prestigious Distinguished Dissertation award. From 1996 to 1999 he was Director of LFCS and he is a founding member of IFIP WG1.3 "Foundations of System Specification". From 2003 to 2011 he was Head of the Informatics Graduate School in Edinburgh with overall responsibility for PhD education.