The program consists of 80-minute lectures.
Arthur Azevedo de Amorim — Rochester Institute of Technology
Introduction to Rocq
The Rocq website contains instructions on how to install all the required packages to follow this introduction. We recommend that you install the Rocq Platform for Rocq v9.0. The website also contains instructions on how to set up popular text editors to develop Rocq code interactively.
Lecture 1 part 1 | part 2 | part 3 | part 4 | part 5 | Notes
Lecture 2 part 1 | part 2 | part 3 | part 4 | part 5 | part 6 | part 7 | Notes
Lecture 3 Notes
Ram Durairajan — University of Oregon
Caught in the Loop: Climate Change and Computing Infrastructure
Climate change and computing infrastructure are becoming increasingly intertwined. On the one hand, climate change and natural hazards increasingly threaten the Internet infrastructure that underpins cloud services and AI. Rising sea levels, solar storms, earthquakes, and wildfires can damage critical infrastructure and lead to large-scale outages. On the other hand, computing itself is becoming a significant environmental challenge. The rapid growth of cloud computing and AI is driving unprecedented demand for energy, water, and physical infrastructure, placing additional pressure on natural resources and contributing to the very environmental changes that threaten these systems. These forces, together, create a feedback loop: climate change impacts computing infrastructure, while the expanding demand for computing can accelerate climate change. This talk highlights both sides of this relationship and discusses how we can build digital infrastructure that is more resilient, sustainable, and prepared for an uncertain future.
Philippa Gardner — Imperial College London
Separation Logic and Compositional Symbolic Execution:
Verification and Bug Detection at Scale
Exercises, Resources, and References
Lecture 1, An Introduction to Separation Logic
Lecture 2, From Separation Logic to Compositional Symbolic Execution
Lecture 3, Compositional Symbolic Execution
Lecture 4, Semi-automatic verification and Automatic Bug Detection
References
Separation Logic: A Logic for Shared Mutable Data Structures John Reynols, LICS’02
Local Reasoning about the Presence of Bugs: Incorrectness Separation Logic, Azalea Raad, Josh Berdine, Hoang-Hai Dang, Derek Dreyer, Peter O'Hearn and Jules Villard, CAV’20.
Compositional Symbolic Execution for Correctness and Incorrectness Reasoning, Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Caroline Cronjäger, Petar Maksimović, and Philippa Gardner, ECOOP’24, distinguished paper.
Compositional Symbolic Execution for the Next 700 Memory Models, Andreas Lööw, Seung Hoon Park, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Opale Sjöstedt, and Philippa Gardner, OOPSLA’25.
Gillian: Compositional testing and verification, Philippa Gardner, a lecture in the course on separation logic organised by Xavier Leroy, College de France, 2021
Simon Gay — University of Glasgow
Session Types and Mailbox Types
Session types and mailbox types are examples of behavioural types, in which a static type system is used to guarantee runtime safety properties that go beyond correct use of data. Typically this means using a type system to specify properties of inter-process communication.
Session types are for point-to-point communication channels. Mailbox types are for actor-style communication with a one-reader-many-writers model and unordered message delivery.
Lecture 1: Introduction to Session Types in Pi Calculus
Lecture 2: Session Types and Functional Programming
Lecture 3: Session Types, Linear Logic and the Curry-Howard Correspondence
Lecture 4: Mailbox Types
References
Simon J. Gay and Vasco T. Vasconcelos. "Session Types". Cambridge University Press, 2025.
Simon J. Gay and Vasco T. Vasconcelos. "Linear Type Theory for Asynchronous Session Types". Journal of Functional Programming, 2010.
Luis Caires and Frank Pfenning. "Session types as intuitionistic linear propositions". CONCUR 2010.
Philip Wadler. "Propositions as Sessions". ICFP 2012, Journal of Functional Programming 2014.
Simon Fowler, Duncan Paul Attard, Franciszek Sowul, Simon Gay and Phil Trinder. "Special Delivery: Programming with Mailbox Types". ICFP 2023; extended version on arXiv 2026.
Herman Geuvers — Radboud University Nijmegen
Introduction to Type Theory
Background on Untyped Lambda Calculus
Introduction to Lambda Calculus
— selected pages by Barendregt and Barendsen.
(This is a selection of pages from the full
Introduction to Lambda Calculus
)
On Type Theory, I hope to basically cover these papers in the course
-
H. Geuvers
Introduction to Type Theory
Language Engineering and Rigourous Software Development (Revised Tutorial Lecture Notes of LerNet ALFA Summer School Piriapolis, Uruguay, 24 February to 1 March, 2008), eds.: Ana Bove, Luis Soares Barbosa, Alberto Pardo, Jorge Sousa Pinto, LNCS 5520, Springer 2009. (This is an improved version.) -
H. Barendregt and H. Geuvers,
Proof Assistants using Dependent Type Systems,
Chapter 18 of the Handbook of Automated Reasoning (Vol 2), eds. A. Robinson and A. Voronkov, Elsevier 2001, pp. 1149 -- 1238.
On Type Theory, extended background material (the full story)
-
Jean-Yves Girard, Yves Lafont, Paul Taylor
Proofs and Types
Cambridge University Press, April 1989 -
Rob Nederpelt and Herman Geuvers
Type Theory and Formal Proof — An Introduction
Cambridge University Press, November 2014.
Inductive Types and Homotopy Type Theory (that I hope to be able to touch upon as well). These sources are good further reads
- The HoTT Book
-
Egbert Rijke
Introduction to Homotopy Type Theory
Cambridge Studies in Advanced Mathematics Cambridge University Press (November 2025)
Lecture 1 part 1 | part 2 | part 3 | part 4 | part 5 | slides 1 | slides 2 | exercises | exercises solutions | Notes 1 | Notes 2
Lecture 2 part 1 | part 2 | part 3 | part 4 | part 5 | part 6 | slides | exercises | Notes
Lecture 3 part 1 | part 2 | part 3 | part 4 | part 5 | slides | exercises | Notes
The Use and Anatomy of an Auto-Active Verifier
Plan for the lectures:
- Writing programs (contracts, invariants)
- Writing proofs (assertions, calculations, induction)
- Building a verifier (architecture, intermediate verification language)
- Language design: Changing the rules
Greg Morrisett — Cornell Tech
Simon Peyton Jones — Epic Games
The Verse Language: Types, Semantics, and Verification
Installing Haskel
- Install ghcup
-
Run
ghcup install ghc -
Run
ghcup install cabal -
Try a quick test: run
ghcito get a REPL description
Elaine Pimentel — University College London
Modal Logic: Proof Theory, Semantics and Applications
Modal logic extends classical logic with operators that allow us to reason about notions such as necessity and possibility, and, more broadly, about concepts such as knowledge, belief, time, obligation, and provability. Because of this expressive power, modal logic plays a central role both in the foundations of logic and in applications across computer science, philosophy, linguistics, and AI, where it is used to model reasoning about information, computation, interaction, and change. This lecture series offers a guided journey from foundational ideas to current themes at the interface of proof theory, semantics, and logic in computer science.
Lecture 1:
Proof theory for classical and intuitionistic logics, with a brief introduction to modal logics
slides |
Lean Code |
Notes
Lecture 2:
Proof theory and Kripke semantics for modal logics
slides |
Lean Code (PCL-prover) |
Lecture 3: Alternative semantic viewpoints, including truth-table and game semantics
Lecture 4: Variations and applications, including non-normal and substructural modal logics
References
- B. F. Chellas, Modal Logic (Cambridge University Press, 1980)
- Patrick Blackburn, Maarten de Rijke and Yde Venema, Modal Logic (Cambridge University Press, 2001)
- Sara Negri and Jan von Plato, Structural Proof Theory (Cambridge University Press, 2001)
- The Modal Cube Revisited: Semantics without Worlds by Renato Leme, Carlos Olarte, Elaine Pimentel and Marcelo E. Coniglio, TABLEAUX 2025
- Efficient Decision Procedures for RNmatrix Semantics by Renato R. Leme, Carlos Olarte, Elaine Pimentel
- Playing with modalities by Elaine Pimentel, Carlos Olarte, Timo Lang, Robert Freiman, Chris Fermüller, LIPIcs, Volume 326, CSL 2025
Useful Links
Nikhil Swamy — Microsoft Research, Redmond
Agentic Proof-oriented Programming
How one can effectively get agents to program and prove correctness using concurrent separation logic