Course pages 2013–14
Nominal Sets and Their Applications
Principal lecturer: Prof Andrew Pitts
Taken by: MPhil ACS, Part III
Prerequisites: Logic and set theory (e.g. Discrete Mathematics I and II from CST Part IA) and operational semantics of typed programming languages (e.g. Semantics of Programming Languages from CST Part IB). Familiarity with some elementary category theory (such as the Category Theory and Logic L108 module).
Names and constructs that bind names are ubiquitous in programming languages. Nominal sets provide a mathematical theory of structures involving names, based on some simple, but subtle ideas to do with symmetry and computing with data structures that are infinite, but finite modulo symmetry. The theory has applications to programming language semantics, machine-assisted theorem proving and the design of functional and logical metaprogramming languages. The course introduces the theory of nominal sets, surveys some of its applications and highlights potential areas for further research.
- Structural recursion and induction in the presence of name-binding operations. [1 lecture]
- Permutations, support and freshness; the category of nominal sets. [2 lectures]
- Name-abstraction; nominal algebraic data types and α-structural recursion. [2 lectures]
- Nominal logic, unification, term-rewriting and logic programming. [2 lectures]
- Functional metaprogramming with name abstractions and local names. [1 lecture]
On completion of this module, students should:
- be familiar with the notion of finitely supported sets, relations and functions
- be able to solve unification problems for nominal algebraic data
- be familiar with forms of structural recursion involving nominal sets of name abstractions and their use in functional metaprogramming.
The lecture material will be assessed by a take-home test, set and marked by the course lecturer. The final module mark will be expressed as a percentage.
Pitts, AM. (2013). Nominal Sets: Names and Symmetry in Computer Science (CUP).
Gabbay, MJ. (2011). Foundations of nominal techniques: logic and semantics of variables in abstract syntax. Article in Bulletin of Symbolic Logic, vol. 17, pp161-229.
Pitts, AM. (2006). Alpha-Structural Recursion and Induction. Article in Journal of the ACM, vol. 53, pp459-506.
Urban, C, Pitts, AM & Gabbay, MJ. (2004). Nominal Unification. Article in Theoretical Computer Science, vol. 323, pp473-497.
Shinwell, MR & Pitts, AM. (2005). Fresh Objective Caml User Manual. University of Cambridge Computer Laboratory Technical Report UCAM-CL-TR-621.