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

FACM FBCS CITP

Contact

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
PGP Key

Research

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.

NominalSetsBook
  • 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:
  • 18th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2015), London, UK, 13-17 April 2015. [PC chair]
  • Mathematical Foundations of Programming Semantics XXXI (MFPS 31) and 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015), Nijmegen, Netherlands, 22-25 June 2015. [Joint invited speaker and MFPS PC member]
  • 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]
  • Cambridge Programming, Logic, and Semantics Group
  • Teaching

    Lecture material for 2014/15 courses:

  • CST Part IA Discrete Mathematics
  • CST Part IB Computation Theory
  • MPhil ACS, CST Part III Category Theory and Logic
  • Project suggestion for 2014/15 CST Part III / MPhil ACS.

    Lecture material for old courses:

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