Next TACL conference and school will be held in Czech Republic in June 2017.
More information available at: http://www.cs.cas.cz/tacl2017/.
Next TACL conference and school will be held in Czech Republic in June 2017.
More information available at: http://www.cs.cas.cz/tacl2017/.
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) |
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:
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.
Lecture 1 video
Lecture 2 video
Lecture 3 video
Lecture 4 video
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: