Bartek Klin

Basic nominal techniques

This introductory course will provide a common basis for other courses. I will explain basic concepts such as atoms, finite support, equivariance, and orbit finiteness, together with their basic properties, plenty of examples and simple motivating applications.

Slides: Part 1, Part 2

Andrew M. Pitts

Nominal sets and functional programming

This course will introduce the category of nominal sets and its applications to functional programming languages featuring structural recursion and induction for data involving name-binding operations.

Slides, Exercises

Mikołaj Bojańczyk

Computation theory with atoms

This course will survey applications of sets with atoms to automata, language and computation theory. We will study various properties that can be expected from the structure of data atoms and the impact of those properties on concepts such as orbit-finiteness, definable sets and notions of computability. The presentation will roughly follow significant parts of the forthcoming book.

Slides: Part 1, Part 2, Part 3

Andrzej Murawski

Nominal game semantics

Game semantics is a robust paradigm for giving semantics to a variety of logical systems and programming languages, with original applications in program analysis and model checking. Nominal game semantics is a recent branch of game semantics that makes it possible to model generative effects (e.g. references, objects, exceptions) by incorporating names (drawn from an infinite set) into play. This course will provide a self-contained introduction to the field along with a brief survey of ongoing more applied work.

Slides: Part 1, Part 2

Maribel Fernández

Nominal rewriting and unification

- Nominal syntax (the role of abstraction, freshness, alpha-equivalence, and extensions)

- Matching and Unification problems (solving equality and freshness constraints)

- Rewriting, Type systems, and Typed Rewriting


Murdoch J. Gabbay

Advanced nominal techniques

This course will be a survey of equivariance, nominal universal algebra and its axiomatisations of the lambda-calculus and first-order logic. Time permitting, I will move on to nominal Stone duality.


Johannes Borgström

Nominal process calculi and modal logics


Sławomir Lasota

Computation theory with atoms II

This will be a continuation of M. Bojańczyk's course. We will study more advanced properties of data atoms (Fraisse atoms, atoms with least supports), as well as more advanced applications (Turing machines, the nominal P vs. NP problem, Constraint Satisfaction Problems).

Slides: Part 1, Part 2