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:
  • 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS2015) and 42nd International Colloquium on Automata, Languages and Programming (ICALP 2015), Kyoto, Japan, 6-10 July 2015. [Invited joint tutorial speaker]
  • British Logic Colloquium 2015, Cambridge, UK, 2-4 September 2015. [Invited speaker]
  • POPL 2016: 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, St. Petersburg, Florida, USA, January 20-22, 2016. [Member of External Reviewing Committee]
  • Cambridge Programming, Logic, and Semantics Group
  • Agda code:
  • Teaching

    Lecture material for 2015/16 courses:

  • CST Part IB Computation Theory
  • CST Part II Types
  • MPhil ACS, CST Part III Category Theory and Logic
  • Project suggestions for 2015/16 MPhil ACS and CST Part III.

    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.)