Location

The winter school will take place from Tuesday 20 January to Friday 23 January, 2026, at University of Twente.

Lectures will take place in the buildings Ravelijn, Carré, and Langezijds.

See these links for building addresses and campus map.

Aims and prerequisites

The Dutch Winter School on Logic and Verification provides classes for PhD/graduate students in theoretical computer science, with a focus on software verification, logic, and type theory. Strong master students, as well as researchers and practitioners, are equally welcome. Participants are expected to have a background in theoretical computer science, mathematics or a related discipline at a master’s level, and have basic familiarity with (functional) programming, semantics, and logic.

Participants that are not from the Netherlands, but for example, from neighboring countries such as Belgium or Germany, are also welcome to attend. The language of the winter school is English.

Courses and lecturers

See below for the abstracts of the lectures.

Organization

The winter school is organized as part of the project Cyclic Structures in Programs and Proofs project (file number OCENW.XL.23.089) of the research program Open Competition Domain Science XL, by the Dutch Research Council (NWO) under the grant https://doi.org/10.61686/FHYZO53064.

The local organizer is Georgiana Caltais.

Registration

Registration will open halfway November. Registration entails a modest fee that covers coffee and lunch, but not dinner nor accommodation.

The number of spots will be limited to 50 participants, registration is first-come first-served.

Accommodation

Accommodation can be booked via websites such as booking.com.

We have arranged some limited block reservations and fixed prices at the following two hotels for the winter school participants. These rooms are available on a first-come, first-served basis. For details about room types etc. please see the hotel websites, or contact the hotel directly. Small deviations in prices may occur in the new year due to inflation and VAT changes. To secure your booking, please follow the instructions below.

U Parkhotel Enschede

Price incl. breakfast and city tax:

  • Comfort room, single occupancy: 139 eur / night;
  • Comfort room, double occupancy: 159 eur / night;
  • Superior room, single occupancy: 149 eur / night;
  • Superior room, double occupancy: 169 eur / night;

Prices are valid until 24 Nov 2025. Reservations must be made by email (bookings@uparkhotel.nl) or phone (+31 5343 31366) and must mention the reference code GA001518.

InterCity Hotel Enschede

Price incl. breakfast and city tax:

  • Standard single room 148 eur / night;
  • Standard double room: 176 eur / night.

Book using the following form in docx or pdf.

Program

A timetable will follow closer to the date of the winter school. Some details:

  • The winter school will start Tuesday 11:00, allowing participants from the Netherlands to travel in the morning.
  • The winter school will end Friday 17:30.
  • During one of the days, we will have a social event.

Abstracts

Causality in Concurrency (Caltais)

This course consists of 1 lecture on concurrency theory, and 1 lecture on actual causality.

Concurrency Theory Concurrent systems are all around us: from multicore processors to distributed networks, yet reasoning about their behaviour remains a fundamental challenge. Concurrency theory provides the mathematical foundations for understanding and verifying such systems. This lecture introduces core concepts through Milner’s Calculus of Communicating Systems (CCS), a seminal process calculus for modelling concurrent interactions. We will explore:

  • The syntax and semantics of CCS processes
  • Various notions of behavioural equivalence and compliance of processes
  • Axiomatisations as a means of reasoning equationally, in a syntactic fashion, about process behaviour
  • Hennessy–Milner Logic for logical characterisations of behavioural properties
  • Together, these concepts form the backbone of formal reasoning about concurrency and provide the theoretical basis from which more advanced topics -such as session types- emerged.

Actual Causality Causality lies at the heart of how we explain and reason about events: we ask not only what happened, but why it happened.

In this lecture, we explore Actual Causality, as formalised by Halpern and Pearl, a rigorous framework for analysing cause-and-effect relationships within complex systems. We will introduce structural causal models, illustrating how they capture dependencies between variables, and discuss how to reason counterfactually within these models.

From a formal verification perspective, causality analysis complements correctness analysis by identifying the variables and events that genuinely caused a property violation. It provides a principled way to explain system failures and to quantify notions such as responsibility, blame, and harm, with applications across ethical, legal, and engineering domains.

Category Theoretical and Coalgebraic Reasoning (Basold and Hansen)

Category theory is an important tool in mathematics, computer science and logic. The central idea of category theory is to shift the focus from individual structures to the relations between those structures. For instance, instead of looking merely at the operations of a vector space, one takes the linear maps between them as the central object of study. This shift in perspective is surprisingly powerful and enables proofs of abstract theorems that apply to a wide range of problems.

In program semantics and formal verification, we often need to reason about systems with potentially infinite or cyclic behaviour such as streams, automata, labelled transition systems, Markov chains or co-recursive types. Coalgebra is an abstract theory (formulated using category theory) for specifying and reasoning about such systems. In particular, coalgebra provides the principle of coinduction, which is formally dual to the well-known principle of induction. Moreover, coalgebraic modal logic is a framework for developing generalisations of Hennessy-Milner logic and temporal logics for a wide range of systems, viewed as coalgebras.

This course provides an introduction to category theory and coalgebra in four lectures:

  1. Basic category theory. We cover the basic concepts such as category, functor, natural transformation, universal properties and adjunctions, illustrated with several examples.
  2. Coalgebra. We define coalgebras and their associated notions of morphism, bisimulation and behavioural equivalence. We also show how final coalgebras give rise to coinduction, and illustrate coinduction with examples such as streams and formal languages.
  3. Coalgebraic modal logic over Set. Set-based coalgebras cover many interesting system types. We show how to define modal logics for such systems via predicate liftings and prove general invariance and expressiveness results in the coalgebraic framework.
  4. Coalgebraic modal logic beyond Set. For coalgebras over base categories other than Set, we cover more abstract approaches to coalgebraic modal logic based on dual adjunctions and fibrations.

Lectures 1,2,4 are taught by Henning Basold. Lecture 3 is taught by Helle Hvid Hansen.

Coinductive Programming and Proving in Agda (Cockx)

Proof assistants based on dependent type theory such as Agda, Rocq, and Lean are typically very good at modeling inductive structures such as lists, trees, or typing derivations. However, to model structures that have cycles or are infinite, we need the lesser well-known counterpart of coinduction. In this series of three lectures, I will introduce the different ways of modeling and reasoning about coinductive structures in the Agda proof assistant, diving into many examples on the way. The lectures will be interactive and are accessible for anyone with basic knowledge of typed functional programming in a language such as Haskell or OCaml.

The first lecture will start with a crash course on Agda, dependently typed programming, and the Curry-Howard correspondence. After this, the course will handle at least the following topics:

  • Using Agda’s coinductive records to model purely coinductive structures such as streams.
  • Using copatterns to define coinductive values.
  • The guardedness criterion for coinductive definitions.
  • Defining and proving bisimilarity of coinductive values.
  • Mixed inductive/coinductive types such as colists and conatural numbers.
  • Using the Delay monad to model potentially non-terminating computations.
  • Working with sized types as an alternative to the guardedness checker.

Depending on the time and audience interest, we can then dive into some deeper topics and case studies:

  • Equational reasoning about formal languages (https://www.cse.chalmers.se/~abela/jlamp17.pdf)
  • Equivalence of bisimulation and equality in Cubical Agda
  • The partiality monad (https://link.springer.com/chapter/10.1007/978-3-662-54458-7_31)
  • Wander types and stream processors (https://www.nii.ac.jp/pi/n10/10_47.pdf)
  • Coinductive graphs (https://doisinkidney.com/pdfs/formalising-graphs-coinduction.pdf)

Session Types (Pérez)

Writing concurrent programs is notoriously difficult. In programs that communicate by exchanging messages over channels, one of the main challenges is ensuring that the sequences of sent and received messages follow a well-defined protocol. Session types address this challenge by providing abstract specifications of channel-based communication protocols. They enable static verification of communication correctness: well-typed programs are guaranteed to respect their intended protocols, avoiding both communication mismatches and deadlocks.

Originally developed within the Concurrency Theory community—as type systems for concurrent processes in the π-calculus—session types have recently attracted growing interest in the Programming Languages community. This increasing attention can be attributed to two main factors:

  • Paradigm independence: session types can be integrated into a variety of programming paradigms, including functional, concurrent, and object-oriented languages.
  • Logical foundations: session types are tightly related (via a Curry–Howard-style correspondence) to Girard’s Linear Logic, providing a rich, bidirectional bridge between logic and programming that continues to inspire new developments.

This course will cover three major themes:

  1. Foundations of session types — syntax, key concepts, and terminology.
  2. Linear logic–based session types (also known as Propositions-as-Sessions).
  3. Advanced topics, including coalgebraic sessions, deadlock freedom by typing, and multiparty sessions.

Program Verification using Concurrent Separation Logic (Krebbers)

Concurrent programs are challenging to get right, especially if threads share access to memory. The formalism of “concurrent separation logic” (which was pioneered by O’Hearn and Brookes in 2007) provides a powerful framework to verify concurrent programs. Over the last 20 years, concurrent separation logic has emerged into an active research field, has been extended with many features (e.g., fine-grained concurrency, weak memory consistency, higher-order programs), been applied to many programming languages (e.g., Rust), and has been implemented in numerous verification tools (e.g., F*, Iris, Verifast, Viper, VST). We will discuss the foundations of separation logic and show how they scale to the verification of challenging concurrent programs.

The course consists of three sessions:

  1. Basic separation logic. We cover the core concepts of separation logic for the verification of imperative programs with pointers. We study the syntax and semantics of separation logic propositions, Hoare triples, and the proof rules (including the “frame” rule).
  2. Concurrent separation logic. We scale up to the verification of concurrent programs. We study the concepts of invariants and ghost state, allowing us to modularly verify tricky programs with shared-memory concurrency.
  3. Advanced topics in separation logic, including the use of separation logic to verify type systems and step-indexing through the later modality.

Exercises and demos using the Iris framework in the Rocq proof assistant will be provided.