TACL school programme

The programme of the school is ready.  We will meet on Monday at 10:50 in the room F6 of the Dipartimento di Matematica (see map below).  We will then walk together to student house; the lectures will then start in the afternoon.


Monday Tuesday Wednesday Thursday Friday
9:00-10:30 Ieke Moerdijk Luke Ong Guram Bezhanishvili Guram Bezhanishvili
10:30-10:50 Coffee Break Coffee Break Coffee Break Coffee Break
10:50-12:20 REGISTRATION Luke Ong Ieke Moerdijk Brian Davey Luke Ong
12:20-13:30 Lunch Break Lunch Break Lunch Break CLOSURE
13:30-15:00 Social Excursion + Social Dinner Brian Davey Ieke Moerdijk
15:00-15:15 Opening Break Break
15:15-16:45 Brian Davey Guram Bezhanishvili Luke Ong
16:45-17:05 Coffee Break Coffee Break Coffee Break
17:05-18:35 Guram Bezhanishvili Ieke Moerdijk Brian Davey
Student session (h20:00, “Sala Riunioni” of the Student House)

Campus map

TACL school: course by Luke Ong

Luke Ong
Title: “Automata, Logic and Games for Higher-Order Model Checking”

Course description: In Part 1 of the course, we introduce the mathematical theory underpinning the model checking of computing systems. The main ingredients are:

  • Automata on infinite trees as a computational model of state-based systems.
  • Logical systems, such as the modal mu-calculus and monadic second-order logic, for describing correctness properties.
  • Two-person games as a conceptual basis for understanding the interactions between a system and its environment.

Some topics: decidability of the MSO theory of the full binary tree, and its consequences; connections between parity games, modal mu-calculus, and alternating parity tree automata, and the sense in which they are equivalent.

Building on these foundations, we discuss, in Part 2, recent developments in high-order model checking, the model checking of infinite trees generated by higher-order recursion schemes (or equivalently lambda-Y calculus). Some topics: decidability of higher-order model checking with respect to modal mu-calculus, and compositional model checking of higher-type Böhm trees.


Lecture notes 1Automata Logic Games 2015

Lecture notes 2Higher-Order Model Checking: An Overview

Slides and more on Luke Ong’s webpage of the course

Lecture 1 video

Lecture 2 video

Lecture 3 video

Lecture 4 video

TACL school: course by Ieke Moerdijk

Ieke MoerdijkTitle: “From algebraic topology to algebraic set theory”

Course description: In the first two lectures, we will discuss several approaches to axiomatic homotopy theory (notably Brown’s Categories of Fibrant Objects and  Quillen’s Model Categories). We will then present a categorical axiomatisation of set theory, in the style of Algebraic Set Theory but directed more towards models of predicative set theory. In a final lecture, we will discuss how one can pass from (models of) the first axiomatisation to the second one. (This last part is based on joint work with Benno van den Berg).

TACL school: course by Guram Bezhanishvili

Guram BezhanishviliTitle of the course: “Frames, topologies, and duality theory”

Course description: Frames are complete lattices that capture the basic features of topologies. The study of frames was initiated in the fifties of the last century. The resulting area is known as pointfree topology. The aim of this course is to present the basics of pointfree topology. The emphasis will be on providing pointfree descriptions of several well-known categories of topological spaces, such as compact Hausdorff spaces and Stone spaces, as well as their non-Hausdorff generalizations, spectral spaces and stably compact spaces. The corresponding categories of frames, as well as the resulting duality theory, will be discussed in detail. The celebrated Stone duality for Boolean algebras and for distributive lattices will be derived as corollaries. Applications of these results to logic will be mentioned towards the end of the course.

Slides lecture 1

Lecture 1 video

Slides lecture 2

Lecture 2 video

Slides lecture 3

Lecture 3 video

Slides lecture 4

Lecture 4 video

TACL school: course by Brian Davey

Warwick Grant

Title of the course: “An invitation to natural dualities in general and Priestley duality in particular”

Course description: “I will assume that participants have a basic knowledge of universal algebra and lattice theory. The course will commence with a discussion of Birkhoff’s Representation for Finite Distributive Lattices (as the lattice of down-sets of a finite ordered set) and work from there to Priestley duality for bounded distributive lattices. Priestley duality will be the stepping off point for an introduction to the theory of Natural Dualities. Applications to Heyting algebras and Ockham algebras will be used to illustrate the theory.

Course material:

Lecture 1 beamer.