Course pages 2012–13
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, survey some of its applications and highlight 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. [1 lecture]
- Functional metaprogramming with name abstractions and local names. [2 lectures]
- Nominal unification, term-rewriting and logic programming. [1 lecture]
- Research directions. [1 lecture]
On completion of this module, students should:
- be familiar with the notion of finitely supported sets, relations and functions;
- be familiar with forms of structural recursion involving nominal sets of name abstractions and their use in functional metaprogramming;
- be able to solve unification problems for nominal algebraic data.
The lecture syllabus will be assessed by a take-home test, set and marked by the principal lecturer. The final module mark will be expressed as a percentage.
Extracts from the draft version of lecturer's forthcoming book Nominal Sets, the metamathematics of names (CUP) will be provided.
Pitts, AM. (2006). Alpha-Structural Recursion and Induction. Article in Journal of the ACM, vol. 53, pp459-506.
Shinwell, MR & Pitts, AM. (2005). Fresh Objective Caml User Manual. University of Cambridge Computer Laboratory Technical Report UCAM-CL-TR-621.
Urban, C, Pitts, AM & Gabbay, MJ. (2004). Nominal Unification. Article in Theoretical Computer Science, vol. 323, pp473-497.
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.