skip to content

Department of Computer Science and Technology

  • Emeritus Professor of Theoretical Computer Science
  • Emeritus Fellow of Darwin College Cambridge


My research makes use of techniques from category theory, mathematical logic and type theory to advance the foundations of programming language semantics and theorem proving systems. I have a long-standing interest in the semantics and logic of names, locality and binding. My aim is to develop mathematical models and methods which aid language design and the development of formal logics for specifying and reasoning about programs. I am particularly interested in higher-order typed programming languages and in dependently typed logics.

Personal web page

On-line publications

Contact Details