Propositions as Sessions: Logical Foundations of Concurrent Computation
This is the webpage for the ESSLLI2024 course on “Propositions as
Sessions”, given by Dan Frumin (d.frumin [the-at-symbol] rug.nl) and Jorge A. Pérez (j.a.perez [the-at-symbol] rug.nl).
The Curry-Howard(-deBruijn) correspondence, also known under the slogan of “Propositions as Types”, is arguably the most important bridge between logic and computation. The connection between intuitionistic logic and lambda-calculus is the most familiar instance of this bridge. The correspondence can be seen as a fruitful principle for logically-informed foundations of programming languages. This introductory course will explore recent work on the Curry-Howard correspondence between substructural logics and concurrent processes, dubbed as “Propositions as Sessions”. Following a gradual approach, participants will learn how Girard’s linear logic and its extensions serve as a basis for structuring message-passing concurrent programs through the discipline of session types. No specific prerequisites are assumed for this course, except for familiarity with formal logic; participants will get familiar with the selected topics in Substructural Logics, Concurrency Theory, and Programming Languages. The course will close with an overview of prospective research challenges.
Schedule / slides
The slides will be uploaded as the course goes on.
- Lecture 1: Introduction and Linear Logic (part 1 .pdf), (part 2 .pdf)
- Lecture 2: Concurrent processes from Linear Logic (slides .pdf)
- Lecture 3: Cut Elimination as Process Communication (slides .pdf)
- Lecture 4: Unrestricted resources, servers, and the !-modality (slides .pdf)
- Lecture 5: The logic of Bunched Implications and its computational interpretation (slides .pdf)
Additional reading
Here is the list of useful references on the topic.
Main references:
- Dual Intuitionistic Linear Logic, Andrew Barber, 1996 (the Linear Logic system DILL)
- Linear Logic Propositions as Session Types, Luis Caires, Frank Pfenning, Bernardo Toninho, 2012 (computational interpretation of intuitionistic linear logic)
- A Bunch of Sessions: A Propositions-as-Sessions Interpretation of Bunched Implications in Channel-Based Concurrency, Dan Frumin, Emanuele D’Osualdo, Bas van den Heuvel, Jorge A. Pérez, 2022
Additional references:
- Introduction to Linear Logic, Torben Brauner, 1996 (lecture notes on linear logic)
- Propositions as Sessions, Philip Wadler, 2012 (computational interpretation of classical linear logic)
See also this webpage with more references on Propositions as Sessions.