home search a-z help
University of Cambridge Department of Computer Science & Technology
Andrew Pitts
Department  of  Computer  Science  & Technology > Andrew Pitts

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



Professor Andrew M Pitts
University of Cambridge
Department of Computer Science & Technology
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


  • On-line publications
  • Recent talks
  • Google Scholar profile
  • ORCiD ID
  • Research

    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.

  • 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 generalisations 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.

  • Editorial activities:
  • Upcoming events:
  • 34th ACM/IEEE Symposium on Logic in Computer Science (LICS 2019), Vancouver, Canada, 24-27 June 2019. [PC member, ToT award]
  • International Conference on Homotopy Type Theory (HoTT 2019), Carnegie Mellon University, Pittsburgh, USA, 12-17 August 2019. [Invited speaker]
  • Nominal Techniques, 3rd School on Foundations of Programming and Software Systems (FoPSS 2019), Warsaw, 10-15 September 2019. [Lecturer, organiser]
  • Théorie des types homotopiques, Ecole de Printemps d'Informatique Théorique (EPIT 2020), Île d'Oléron, France, 25-29 May 2020. [Lecturer]
  • Agda code
  • Cambridge Programming, Logic, and Semantics Group
  • Teaching

    Lecture material for 2018/19 courses:

  • CST Part IB Computation Theory
  • CST Part II Denotational Semantics
  • MPhil ACS, CST Part III Category Theory
  • Lecture material for old courses:

  • Types (Last used for 2016/17 CST Part II.)
  • 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.)
  • Semantics of HOT Languages (Last used for 2009/10 MPhil ACS.)
  • Semantics of Programming Languages (Last used for 2001/02 CST Part IB.)