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 1: Automata Logic Games 2015

Lecture notes 2: Higher-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

Title: “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).

Title 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