Abstract: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 contexts, with global types using this projection and subtyping relations, and prove an operational correspondence between a local type context and its associated global type. We utilise this association relation to prove the safety and liveness of associated local type contexts and, consequently, the multiparty sessions typed by these contexts.
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 this https URL .
| Comments: | To appear in the proceedings of ITP 2026 |
| Subjects: | Logic in Computer Science (cs.LO) |
| ACM classes: | F.1.2; F.3.1; F.3.3; F.4.1 |
| Cite as: | arXiv:2605.23633 [cs.LO] |
| (or arXiv:2605.23633v1 [cs.LO] for this version) | |
| https://doi.org/10.48550/arXiv.2605.23633 arXiv-issued DOI via DataCite (pending registration) |
From: Omer Keskin [view email]
[v1]
Fri, 22 May 2026 13:50:10 UTC (172 KB)
此内容由惯性聚合(RSS阅读器)自动聚合整理，仅供阅读参考。 原文来自 — 版权归原作者所有。