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 formal languages that is based upon symmetry. They have many applications to the syntax and semantics of programming language constructs that involve binding, or localising names and to logics that underly systems for machine-assisted reasoning about programming language semantics.

    Book: Nominal Sets: Names and Symmetry in Computer Science.

    Mark Shinwell and Andrew Pitts' Fresh O'Caml functional programming language.

    James Cheney and Chrisitain Urban's αProlog logic programming language.

    Christian Urban and Stefan Berghofer's Nominal package for Isabelle/HOL.

    Dominic Mulligan's CiteULike library on Nominal Techniques

    Christian Urban's Nominal Bibliography

  • 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:
  • 17th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2014), Grenoble, France, 6-13 April 2014. [PC member]
  • 20th Conference "Types for Proofs and Programs" (TYPES 2014), Institut H. Poincaré (IHP), Paris, 12-15 May 2014. [Invited speaker]
  • 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]
  • 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
  • Project suggestion for CST Part II 2013/14.

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