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:
  • 29th ACM/IEEE Symposium on Logic in Computer Science joined with the 23rd EACSL Annual Conference on Computer Science Logic (CSL-LICS 2014), Vienna, 14-18 July 2014. Part of the Vienna Summer of Logic, 9–24 July 2014. [PC member]
  • 9th Logical and Semantic Frameworks, with Applications (LSFA 2014), Brasília D.F., Brazil, 8-9 September 2014. [Invited speaker]
  • 18th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2015), London, UK, 13-17 April 2015. [PC chair]
  • 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 tutorial]
  • Cambridge Programming, Logic, and Semantics Group
  • Teaching

    Lecture material for 2013/14 courses:

  • CST Part IA Discrete Mathematics
  • CST Part IB Computation Theory
  • CST Part II Types
  • MPhil ACS, CST Part III Nominal Sets and Their Applications
  • Lecture material for old courses:

  • Denotational Semantics (Last used for 2011/12 CST Part II.)
  • 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.)