TACL 2019 Summer School

Île de Porquerolles,  10 - 15 June 2019

The summer school is a satellite event of the TACL 2019 conference. Both events focus on logic and the tools provided by topology, algebra, and category theory. Hence the name TACL, for Topology, Algebra, and Categories in Logic. TACL conferences and schools provide a healthy environment for interactions between computer scientists and mathematicians working in logic. The TACL conference has been held every two years since 2003 and since 2013 a summer school, such as the present one, has been associated to the conference.

The week is organized around four advanced lectures on central themes of TACL. Each lecture consists of five sessions of one hour and two exercise sessions of two hours each. Besides, one or two sessions of short presentations (15 minutes + questions) and a poster session will be organized.


The summer school will take place in the week before the conference. The arrival on the island will be on Monday 10 June 2019, in the afternoon/evening. Then, the school’s programme will start on Tuesday 11 June 2019 in the morning and will end on Saturday 15 June 2019 in the afternoon. A bus transfer from and to Nice will be arranged by the organizers. Please be warned that most people will need to be accommodated in a room shared with 1-3 other summer school participants.

Programme of the school

Travel to the island

The bus from Nice will depart from the airport at 15:00 on Monday, 10 June 2019. We are hoping to arrive to Tour Fondue before 17:30 so that we can catch the second to last boat of the day to Porquerolles. Participants should arrive well in advance of this time.

If you are planning to arrive to the island by yourself, please note that the last boat departs of the day leaves at 18:30. For more information see maritimes bateau website.

There will be a dinner prepared for us in Porquerolles upon arrival to the venue.

Departure from the island

We are planning that the programme of the school will end just in time for the boat that leaves Porquerolles at 17:00 on Saturday. Then, there will be two buses arranged for those participants who are coming to Nice.

On the departure day the last provided meal at the venue will be the lunch at 12:30. However, it is expected that the participants will be able to buy some snacks at one of the rest stops on the way to Nice.

The venue

To see what Île de Porquerolles is like, go to hyeres-tourisme.com. The address of the venue is as follows:

Hôtel Club IGESA
Rue de la Douane
Ile de Porquerolles
83 400 HYERES
(for more see igesa.fr)

Meal times

Breakfast 07:15-09:15
Lunch 12:15-13:15
Dinner 19:15-20:15

Important dates

Pre-registration deadline:
Reduced fee request by:
31 March 2019
31 March 2019
Notification: 10 April 2019
Final registration and payment: 30 April 2019

For more information about pre-registration and registration, go to registration page.


Maria Manuel Clementino
Coimbra University

Title: Category Theory


As stressed in the name of this series of conferences, Algebra, Category Theory, and Topology play important roles in the study of Logic. This course intends to introduce the basic notions and methods of Category Theory, illustrating them with applications to Algebra, Topology, and Logic. It is also meant as a warm-up to the following course in Categorical Logic.

The course is divided in 5 one-hour lectures, and 4 hours of exercises. The lectures will focus on:

  1. Categories, functors, and natural transformations
  2. Limits and colimits
  3. Presheaves and the Yoneda Lemma
  4. Adjoint functors
  5. Cartesian closed categories and elementary toposes.

André Joyal
University of Quebec - Montreal

Title: Topos Theory


What is first order logic? The answer depends on your philosophy and your purpose. My goal is to present the algebraic structure of first order logic. In three kinds: geometric, intuitionistic and classical. We shall use the notion of first-order logical doctrine for this purpose (it is a special case of the notion of hyper-doctrine by F.W. Lawvere). The notion of frames and topos theory will play an important role in the description (I will not suppose that the participants are familiar with topos theory). A pre-doctrine is defined to be a functor

P: FinPoset

where Fin denotes the category of finite sets and Poset denotes the category of partially ordered sets. A geometric doctrine is pre-doctrine satisfying a few more conditions; similarly for the notions of Heyting doctrine and of boolean doctrine. The latter constitute a complete algebraic description of classical first-order predicate logic (like the notion of boolean algebra for classical propositional logic). I will introduce the notion of model of a geometric doctrine, and the notion of morphism between models. If times permits, I will introduce the classifying topos of a geometric doctrine.

The course is divided into 5 sessions of 1 hour, with 4 hours of exercises.

  1. On frames, Heyting algebras and Boolean algebras;
  2. Presheaf toposes, algebra of relations in a topos;
  3. Pre-doctrines, quantifiers and the equality relation;
  4. The doctrines of geometric logic, of Heyting logic and of boolean logic;
  5. Models and classifying toposes.


  • B. Jacobs, Categorical logic and type theory, North-Holland, 1999.
  • P.T. Johnstone, Sketches of an Elephant, Oxford, 2002.
  • A. Kock & G. E. Reyes, Doctrines in Categorical Logic, Handbook of Math. Logic, 1977.
  • F.W. Lawvere, Equality in hyperdoctrines and the comprehension schema as an adjoint functors, AMS, 1970.
  • J. Picado & A. Pultr, Frames and Locales, Birkhäuser, 2012.
  • A. M. Pitts, Tripos theory in retrospect, Math. Struc. in Comp. Sci, 2002.
  • R.A.G. Seely, Hyperdoctrines, natural deduction and the Beck condition, Zeitschrift, 1983.
  • Todd Trimble, Notes on predicate logic, nLab.

George Metcalfe
University of Bern

Title: Bridges between Algebra and Logic
Slides: part 1, part 2, part 3, part 4


This course will be about building and crossing (in both directions) bridges between the fields of algebra — understood, crudely, as the study of structure — and logic, understood, again crudely, as the study of consequence. Such bridges can be beneficial for practitioners of both disciplines. Indeed, in favourable cases, results obtained in one domain can be imported directly into the other using so-called “bridge theorems”. For example, algebraic properties such as coherence, amalgamation, and the congruence extension property for a class of algebras are closely related to properties of equational consequence such as (uniform) interpolation and existence of a deduction theorem. In this course, we will consider these and other properties first in the setting of intuitionistic logic and Heyting algebras (including Pitts’ uniform interpolation theorem), and then in the more general setting of universal algebra. A wide range of examples and applications will be given throughout the course, spanning, in particular, classes of lattices and (ordered) groups, modal logics, and substructural logics.

Yde Venema
University of Amsterdam

Title: Duality Theory
Course notes: 1-introduction.pdf, 2-generalizations.pdf, 3-modal-duality.pdf, 4-duality-and-logic.pdf


Duality is a fundamental principle that reveals deep connections between algebraic and geometrical ways of approaching mathematics. As its manifestation in logic and computer science, duality theory builds bridges between syntax and the structures that interpret it, and between deductive systems and their relational/topological semantics. The term `duality’ is often used in a rather intuitive sense, but it can be made mathematically precise in category theory, where a duality is a contravariant equivalence between two categories.

The course will give a first introduction to the role of duality theory in propositional logic. We will focus on the structures that feature in algebraic logic, such as Boolean algebras, distributive or modal algebras, and the spatial (i.e., relational/topological) structures that provide the semantics of the corresponding logics. In the first part of the course we will discuss various examples of categorical dualities, starting with Stone’s duality for Boolean algebras. In the second part we will see how to use these dualities by connecting and comparing algebraic and spatial concepts. Examples include the notions of correspondence and canonicity, subdirect irreducibility, and the Vietoris construction.

Below is a tentative table of contents:

  1. Basis: Stone duality for Boolean algebras.
  2. Variations: distributive lattices, Heyting algebras and frames.
  3. Extensions: modal algebras
  4. Connections: correspondence and canonicity
  5. Transfer: subdirect irreducibility and the Vietoris construction.
Prerequisites: Some familiarity with (propositional) logic, (Boolean) algebras, and basic topology will be presupposed; prior exposure to modal logic will be useful, but not essential.