Location

After a successful first iteration, we are organising the winter school this time in Leiden. It will take place from Monday, 18 January to Friday, 22 January 2027, at Leiden University in the Gorleaus Building.

The Gorleaus building can be reached by bus, either via the Universiteitsterrein stop or the Bio Science Park-Oost stop. These are both served by frequent busses from the Leiden Centraal bus terminal.

Organisation and Contact

The winter school is organised as part of the project Cyclic Structures in Programs and Proofs (file number OCENW.XL.23.089) of the research program Open Competition Domain Science XL, by the Dutch Research Council (NWO).

The local organisers are Henning Basold and Sarah Dukic. If you have questions about the winter school, please send an e-mail to the organisers.

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.

The language of the winter school is English and participants from outside the Netherlands are of course warmly welcome to attend.

Courses and lecturers

The programme will comprise two parallel tracks: one with foundational courses and one with advanced courses. Each course will have lectures and working groups to deepen the understanding. Each day will end with a short highlights talk by a researchers, in which the relevance of the course material is demonstrated in their research. We will also have a plenary session, in which the participants can ask and discuss openly with the lecturers.

The school will have the following courses and highlights talks. Details on lecturers and content will be announced soon.

Foundational Track

Advanced Track

Highlights Talks

  • Real World Proof Formalisation
  • MetaRocq and Correctness of Proof Assistants
  • Coalgebras in Concurrency and Behavioural Types
  • Cyclic Proofs in Scientific Practise

Programme

Below you may find the tentative timetable for the graduate school. Each lecture is always followed by a break and the corresponding working group, with the exception of the first lectures on Monday at 10:30, which have no working group attached.

Time Monday Tuesday Wednesday Thursday Friday
9:00 – 10:30 09:30 – 10:00 Registration Lecture Lecture Lecture Lecture
10:30 – 11:00 10:00 – 10:30 Welcome Break Break Break Break
11:00 – 12:00 10:30 – 12:00 Lecture Working group Working group Working group Working group
12:00 – 13:30 Lunch Lunch Lunch Lunch Lunch
13:30 – 15:00 Lecture Lecture Lecture Lecture Working group
15:00 – 15:30 Break Break Break Break 15:00 End of school
15:30 – 16:30 Working group Working group Working group 15:30 – 16:00 Highlights talk  
16:30 – 17:00 Highlights talk Highlights talk Highlights talk 16:00 – 17:30 Plenary discussion  
    17:00 – 19:00 Reception   19:00 Dinner  

Registration

The registration will open 9 November 2026 and can be done via the registration page. The deadline for early registration is 14 December 2026 and 7 January 2027 for late registration. Participation fees are 200€ (early registration) and 250€ (late registration) per participant. These fees include lunch, refreshments in breaks, a reception on Tuesday and the social dinner on Thursday.

Certificates of participation can be provided.

Accommodation

Participants are expected to arrange accommodation themselves.

The Leiden University has special arrangement with the following hotels, in increasing ascending order of price ranging from 122€ - 155.79€ per night for one person including breakfast. If you book with these hotels, then you need to indicate with the hotel that you wish to use the agreement with Leiden University.