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.

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.

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**

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.

- 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

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.

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