Workshop · IT University of Copenhagen · 15–16 September 2026

Workshop on Probabilities and Session Types

A small, informal workshop bringing together researchers working on probabilistic extensions of session types and related behavioural type theories. The format alternates talks with discussions and working groups, with the second day devoted to open problems and possible joint funding applications.

Dates
15–16 September 2026 (1.5 days)
Venue
Room 3A20, IT University of Copenhagen (ITU), Rued Langgaards Vej 7, 2300 Copenhagen S — see how to find us
Organisers
Marco Carbone (ITU), Maria Bendix Mikkelsen (ITU) and Nobuko Yoshida (University of Oxford)

Programme

Day 1 Tuesday 15 September

09:00–09:10
Welcome
09:10–09:30
Paired conversations
09:30–09:55
Pair introductions
09:55–10:25
Probabilistic session-type monitoringAlceste Scalas · DTU
10:30–11:00
Coffee
11:00–11:30
On deep combine for binary probabilistic session typesMarco Carbone · ITU
11:30–12:00
Global Probabilistic Multiparty Session TypesMaria Bendix Mikkelsen · ITU
12:00–13:00
Lunch (own expense)
13:00–13:30
Probabilistic Multiparty Session Types with Probabilistic BisimulationLitu Zou · Oxford
13:30–14:00
Model checking probabilistic multiparty session typesAleksander Junge · Oxford
14:00–14:30
On Causality in Quantum ComputingKirstin Peters · Augsburg
14:30–15:00
Plenary: collecting sub-topics
15:00–15:30
Coffee and cake
15:30–16:30
Working groups
16:30–17:00
Report back
18:30
Dinner (own expense)

Day 2 Wednesday 16 September

09:00–10:30
Sub-topic discussions
10:30–11:00
Coffee
11:00–11:40
Funding opportunities and joint proposals
11:40–12:00
Actions and closing
12:00–13:00
Lunch (own expense)

Abstracts

On deep combine for binary probabilistic session types

Marco Carbone · ITU

Abstract to follow. The talk also introduces the work of Inverso et al. on probabilistic binary session types.

↑ Back to programme

Model checking probabilistic multiparty session types

Aleksander Junge · University of Oxford

We exhibit a probabilistic multiparty session calculus, as well as an accompanying MPST type system. The type system follows the bottom-up approach of checking safety and liveness by model checking: we export the composition of individual local types of the session into PRISM modules and model check their interleaving. The type system takes safety to be the only required ‘sure’ property and permits ‘partial correctness’ on deadlock-freedom and liveness, i.e. the model checking simply returns lower bounds for the probability with which these properties hold. The talk focuses on implementation aspects such as type inference and PRISM property encodings, in particular liveness, which took some work to get right, as PRISM’s notion of fairness was too crude to utilize directly.

↑ Back to programme

Global Probabilistic Multiparty Session Types

Maria Bendix Mikkelsen · ITU

Session types can be extended with probabilities, so that a protocol says not only who sends what to whom, but how likely each branch is. One thing a type can then compute is the probability that the protocol succeeds. Inverso et al. do this for binary sessions, typing a probabilistic choice by combining two typing contexts. We report on carrying this to the multiparty setting, typing processes directly against global types rather than projecting to local types. Here, a participant that takes no part in a communication cannot see which way it went. The weights it sees afterwards are marginals over the branches, and observing them tells it something about which branch was taken. So the probabilities depend on who is looking, and the design question is what a global type should record. We describe two approaches: 1. computing the marginal, by erasing the communications a participant cannot see and combining the remaining branches, and 2. storing both branches in a constructor that is never simplified. The first leaves types as protocols in the ordinary sense, but makes the metatheory hard, for reasons we will state. The second treats types as mixtures of protocols instead, and is mechanised in Rocq. Recursion is current work.

↑ Back to programme

On Causality in Quantum Computing

Kirstin Peters · University of Augsburg

Abstract to follow.

↑ Back to programme

Probabilistic Multiparty Session Types with Probabilistic Bisimulation

Litu Zou · University of Oxford

Session types are behavioural types whose states evolve through communication between processes. When randomness or uncertainty is present, conventional session typing—based primarily on communication structure—does not provide sufficient semantic compositionality. A richer, semantics-based approach is needed to verify both totally and partially correct processes. This talk presents a methodology for integrating probabilistic bisimulation into a probabilistic multiparty session type system.

↑ Back to programme

Participants

Venue

The workshop takes place in room 3A20 at the IT University of Copenhagen, Rued Langgaards Vej 7, 2300 Copenhagen S (map).

On arrival, please check in at the ITU reception: the staff there will tell you how to find the room.