home search a-z help
University of Cambridge Computer Laboratory
Andrew Pitts
Computer Laboratory > Andrew Pitts

Andrew Pitts Professor of Theoretical Computer Science
Fellow of Darwin College, Cambridge



Professor Andrew M Pitts
University of Cambridge
Computer Laboratory
William Gates Building
15 JJ Thomson Avenue
Cambridge CB3 0FD, UK

Office: FC08
Tel: +44 1223 334629
Fax: +44 1223 334678
Email: Andrew.Pitts at cl cam ac uk


I am interested in all aspects of programming language semantics, be they operational or denotational (or somewhere between the two). My research makes use of techniques from mathematical logic, type theory and category theory to advance the foundations of programming language semantics. The aim is to develop mathematical models and methods which aid language design and the development of formal logics for specifying and reasoning about programs, with an emphasis on higher order, typed programming languages, such as ML and Haskell. I have a long-standing interest in the semantics and logic of names, locality and binding.

  • Nominal Sets provide a promising new mathematical analysis of names in computer science that is based upon symmetry. They have applications to the syntax and semantics of programming language constructs that involve binding and localising the scope of names; to logics that underly systems for machine-assisted reasoning about programming language semantics; and to the automatic verification of process specifications in nominal calculi for concurrency (such as π-calculus). Nominal sets and their generalizations are being applied to automata theory over infinite alphabets with applications to querying XML and databases. Nominal sets also feature in recent work on the cubical sets model of Homotopy Type Theory and univalent foundations.

  • On-line publications. Google Scholar profile. BiBTeX file.
  • Recent talks
  • Recent research projects:
  • Computational Applications of Nominal Sets (CANS).
  • FreshML: A Fresh Approach to Name Binding in Metaprogramming Languages.
  • Editorial activities:
  • Upcoming events:
  • Big Proof, a six week programme at the Isaac Newton Institute for Mathematical Sciences, Cambridge UK, 26 June - 4 August 2017. [Organiser]
  • Cambridge Programming, Logic, and Semantics Group
  • Agda code:
  • Teaching

    Lecture material for 2016/17 courses:

  • CST Part IB Computation Theory
  • CST Part II Types
  • MPhil ACS, CST Part III Category Theory and Logic
  • Lecture material for old courses:

  • Discrete Mathematics (Last used for 2014/15 CST Part IA.)
  • Nominal Sets and Their Applications (Last used for 2013/14 MPhil ACS, CST Part III.)
  • Regular Languages and Finite Automata (Last used for 2012/13 CST Part IA.)
  • Denotational Semantics (Last used for 2011/12 CST Part II.)
  • Semantics of HOT Languages (Last used for 2009/10 MPhil ACS.)
  • Semantics of Programming Languages (Last used for 2001/02 CST Part IB.)