Andrew M. Pitts
Department of Computer Science & Technology
University of Cambridge
United Kingdom
An introduction to nominal sets
Abstract
Nominal sets provide a mathematical foundation for a large body of work motivated by an important question in computer science to do with constructs involving names: when is a mathematical structure used to model some form of computation dependent upon, or independent from, some given names? The theory is based on some simple, but subtle ideas to do with permutations of names and the notion of "finitely supported" mathematical structures, which first arose in mathematical logic in the 1930s. About 20 years ago the lecturer and Jamie Gabbay showed that this can provide a mathematical theory and an accompanying logic for some of the key concepts to do with representing and computing with data involving bound names, such as freshness, abstraction and scoping of names (for which work they were given the Alonzo Church Award in 2019). Since then the theory has been generalised and applied, becoming a fundamental tool for understanding locality in models of computation and programming languages. It has applications to the syntax and semantics of programming languages, to logics for machine-assisted reasoning about programming-language semantics, to the automatic verification of specifications in process calculi and to automata theory over infinite alphabets, with applications to querying XML and databases.
The lectures will introduce the theory of nominal sets and survey some of its applications, particularly in the realm of functional programming.
Course materials
- A. M. Pitts. An introduction to nominal sets. Slides from EWSCS 2020.
- A. M. Pitts. Exercise class problems from EWSCS 2020, with solutions for some. [pdf]
- Videos from the lectures (large, unedited files) [mp4, password-protected]
- A. M. Pitts. Nominal Sets: Names and Symmetry in Computer Science. Cambridge Tracts in Theoretical Computer Science, v. 57, xiv+276 pp. Cambridge Univ. Press, 2013. [doi] Draft version of some chapters. [pdf, password-protected]
- A. M. Pitts. Alpha-structural recursion and induction. J. ACM, v. 53, n. 3, pp. 459-506, 2006. [doi]
- A. M. Pitts, J. Matthiesen, J. Derikx. A dependent type theory with abstractable names. Electron. Notes Theor. Comput. Sci., v. 312 (I. Mackie, M. Ayala-Rincon, eds., Proc. of 9th Wksh. on Logical and Semantic Frameworks with Applications, LSFA 2014), pp. 19-50, 2015. [doi]
- M. Bojańczyk. Slightly Infinite Sets: The "Atom Book". 2019. [pdf]
Last changed
April 10, 2020 22:30 Europe/Helsinki (GMT +03:00)
by
local organizers, ewscs20(at)cs.ioc.ee
EWSCS'20 page:
//cs.ioc.ee/ewscs/2020/