Formally verified liveness with multiparty session types in Rocq

Conference item

Multiparty session types (MPST) offer a framework for the description of communication-based protocols involving multiple participants. In the top-down approach to MPST, the communication pattern of the session is described using a global type. Then the global type is projected on to a local type for each participant, and the individual processes making up the session are type-checked against these projections. Typed sessions possess certain desirable properties such as safety, deadlock-freedom and liveness.

In this work, we present the first mechanised proof of liveness for synchronous multiparty session types in the Rocq Proof Assistant. Building on recent work, we represent global and local types as coinductive trees using the Paco library. We use a coinductively defined subtyping relation on local types together with another coinductively defined plain-merge projection relation relating local and global types. We then associate collections of local types, or local type environments, with global types using these projection and subtyping relations, and prove an operational correspondence between a local type environment and its associated global type. We utilise this association relation to prove the safety and liveness of associated local type environments and, consequently, the multiparty sessions typed by these environments.

Besides clarifying the often informal proofs found in the MPST literature, our Rocq mechanisation also enables the certification of liveness properties of communication protocols. Our contribution amounts to around 14K lines of Rocq code, available at https://github.com/omerskeskin/ mpstlive.

Authors: Keskin, O; Yoshida, N; van Glabbeek, R

• Publication status: Accepted
• Peer review status: Peer reviewed
• Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany
• Host title: Leibniz International Proceedings in Informatics
• Pages: 4:1–4:21
• Article number: 4
• Publication date: 2026-05-24
• Acceptance date: 2026-04-26
• Event title: 17th International Conference on Interactive Theorem Proving (ITP 2026)
• Event location: Lisbon, Portugal
• Event website: https://itp-conference-2026.github.io/index.html
• Event start date: 2026-07-26
• Event end date: 2026-07-29
• Language: English
• Keywords: multiparty session types; liveness; safety; fairness; deadlock-freedom; endpoint projection; subtyping; Rocq; coinduction; property verification