Asynchronous Multiparty Sessions with Mixed Choice

Franco Barbanera (University of Catania); Mariangiola Dezani-Ciancaglini (University of Torino)

arxiv: 2604.06872 · v1 · submitted 2026-04-08 · 💻 cs.LO

Asynchronous Multiparty Sessions with Mixed Choice

Franco Barbanera (University of Catania) , Mariangiola Dezani-Ciancaglini (University of Torino) This is my paper

Pith reviewed 2026-05-10 17:06 UTC · model grok-4.3

classification 💻 cs.LO

keywords multiparty sessionsmixed choiceasynchronous communicationtype systemscoherencelock freedomorphan messagesglobal types

0 comments

The pith

Coherence of communication label sets ensures that typable asynchronous multiparty sessions with mixed choice are lock-free and orphan-message-free.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces a type system for an asynchronous calculus of multiparty sessions that supports mixed choices, allowing nondeterministic selection of both input and output prefixes at each step. It builds typing judgments from global types equipped with a coinductive labelled transition system, using coherence of label sets as the key condition: such a set must contain either every communication enabled in the current session or every action currently shown by one participant, while guaranteeing at least one input for each expected sender. This yields proofs of subject reduction and session fidelity for well-typed sessions. Those two properties together establish that typable sessions never deadlock and never leave messages undelivered. The work further shows how a modest extension of the type system can guarantee eventual reception.

Core claim

Global types with a coinductive labelled transition system and a type discipline based on coherence of communication label sets allow typing of multiparty sessions with mixed choice. Typable sessions satisfy subject reduction and session fidelity, which together imply that they are both lock-free and orphan-message-free.

What carries the argument

Coherence for sets of communication labels, defined so that a set contains either all enabled communications in the session or all actions exhibited by one participant provided at least one input is enabled for each expected sender.

If this is right

Subject reduction holds for the typing relation.
Session fidelity is preserved under reduction in typable sessions.
No typable session can reach a locked configuration.
No typable session can produce an orphan message that is never received.
An extension of the type system can additionally enforce eventual reception of every message.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The coherence condition might be reused to establish other progress properties such as bounded buffering or termination under fairness assumptions.
The orthogonality to projection-based methods suggests the approach could be combined with existing global-type tools to handle protocols that mix choice and asynchrony.
Because the definition is coinductive, it may scale to infinite or recursive session descriptions without requiring finite-state restrictions.

Load-bearing premise

The chosen definition of coherence for communication label sets is sufficient to guarantee lock-freedom and orphan-message-freedom for every session that can be typed under the coinductive transition relation.

What would settle it

A concrete example of a multiparty session that receives a valid typing derivation under the coherence rules yet reaches a state in which every participant is blocked awaiting an unavailable action, or in which a sent message remains unconsumed by its intended receiver, would falsify the safety claims.

read the original abstract

We present an asynchronous calculus for multiparty sessions with mixed choice, which extends the Simple MultiParty Session framework in order to support nondeterministic choices with both input and output prefixes. Global types -- equipped with a coinductively defined labelled transition system -- form the basis of a type system that exploits the key notion of coherence of communication label sets. Roughly, a coherent set contains either all the communications enabled in the session, or all the actions currently exhibited by a participant, provided that at least one input is enabled for each expected sender. Our approach to the typing of multiparty sessions is orthogonal to the well-established, projection-based approaches of the MultiParty Session Type framework. We prove fundamental theorems for typable multiparty sessions, including Subject Reduction and Session Fidelity. These properties imply that typable sessions are both Lock-Free and Orphan-Message-Free. We also investigate the Eventual Reception property for an extension of the type system. Some examples demonstrate the expressiveness of mixed choice in asynchronous multiparty protocols and the effectiveness of the proposed type discipline.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper extends async multiparty sessions to mixed choice via coherence on label sets rather than projection, and states SR plus fidelity theorems that imply lock-freedom and orphan-message-freedom.

read the letter

The core advance is adding nondeterministic mixed choice (input or output prefixes) to the Simple MultiParty Session framework in an asynchronous setting. They equip global types with a coinductive LTS and type sessions using a coherence predicate on communication label sets, which is meant to be orthogonal to the usual projection methods. The abstract reports that typable sessions satisfy Subject Reduction and Session Fidelity, from which lock-freedom and orphan-message-freedom follow, plus some work on eventual reception in an extension. That combination of features is not in the cited prior literature, so the result is new within the subfield. The approach looks useful for protocols that need flexible choice without forcing a global-to-local projection step. The examples are said to show the added expressiveness, which is the practical payoff. The coherence definition is only sketched roughly, and the stress-test note flags a possible gap: in an async mixed-choice LTS, it is not obvious that the predicate (all enabled communications or all actions of a participant with the input proviso) automatically rules out orphan messages under coinductive transitions. Because the method avoids projection, there is no separate syntactic matching check to fall back on, so the entire safety burden sits on how coherence interacts with buffering and nondeterminism. Without the full proof details it is hard to judge whether the clauses close every case. This is niche work aimed at concurrency theorists who already know session types. A reader looking for new typing disciplines for expressive async protocols would find the idea and the stated theorems worth examining. The paper is coherent on its own terms and engages the literature directly, so it deserves a serious referee who can check the coinductive definitions and the implication steps. I would send it out for review rather than desk-reject.

Referee Report

1 major / 1 minor

Summary. This paper develops an asynchronous calculus for multiparty sessions that incorporates mixed choice, allowing nondeterministic selections involving both input and output actions. It employs global types equipped with a coinductively defined labelled transition system and introduces a coherence predicate on sets of communication labels. The type system is designed to be orthogonal to traditional projection-based methods in multiparty session types. Key results include proofs of Subject Reduction and Session Fidelity, which are shown to entail that typable sessions are lock-free and free of orphan messages. The work also explores an extension for the Eventual Reception property and provides examples of its expressiveness.

Significance. Should the proofs of Subject Reduction, Session Fidelity, and the derived safety properties hold under the proposed coherence notion, this contribution would be significant for the field of session types. It broadens the applicability of multiparty session types to protocols with mixed choices in asynchronous environments, which are common in practice. The orthogonality to projection offers an alternative typing strategy that may simplify certain analyses. The coinductive LTS supports reasoning about recursive and infinite sessions, and the explicit derivation of lock-freedom and orphan-message-freedom from the core theorems is a strength.

major comments (1)

The central claim that typable sessions are Lock-Free and Orphan-Message-Free rests on Subject Reduction and Session Fidelity, which in turn depend on the coherence predicate for communication label sets. The rough definition provided—that a coherent set contains either all enabled communications or all actions by a participant with at least one input enabled for each sender—requires precise formalization to ensure it precludes orphan messages in the presence of asynchronous buffering and mixed choices under the coinductive LTS. A potential gap here would undermine the implication to orphan-message-freedom.

minor comments (1)

The qualifier 'roughly' for the coherence definition should be removed or the full definition referenced to enhance precision in the summary.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their careful reading of the manuscript and for their positive evaluation of its significance. We address the single major comment below.

read point-by-point responses

Referee: The central claim that typable sessions are Lock-Free and Orphan-Message-Free rests on Subject Reduction and Session Fidelity, which in turn depend on the coherence predicate for communication label sets. The rough definition provided—that a coherent set contains either all enabled communications or all actions by a participant with at least one input enabled for each sender—requires precise formalization to ensure it precludes orphan messages in the presence of asynchronous buffering and mixed choices under the coinductive LTS. A potential gap here would undermine the implication to orphan-message-freedom.

Authors: We agree that clarity on the coherence predicate is essential, as it underpins the safety results. The manuscript gives a formal coinductive definition of coherence (Definition 3.7) on sets of labels, which is not merely the rough description in the abstract. This definition is used directly in the statements and proofs of Subject Reduction (Theorem 4.5) and Session Fidelity (Theorem 4.8). The proofs proceed by induction on typing derivations and reduction steps; at each step the coherence invariant is preserved, ensuring that any buffered message has a matching enabled input (preventing orphans) and that no participant is permanently blocked (preventing locks). Orphan-message-freedom is then obtained as Corollary 4.10 and lock-freedom as Corollary 4.11. The coinductive LTS and the mixed-choice rules are accounted for in the case analysis. To improve readability we will expand the informal explanation immediately after Definition 3.7 and add a short paragraph in the proof of Corollary 4.10 that explicitly traces how coherence rules out orphan messages under asynchrony. This is a presentational clarification; the technical content and proofs remain unchanged. revision: partial

Circularity Check

0 steps flagged

No significant circularity; proofs rely on independent coinductive reasoning

full rationale

The paper introduces a coherence predicate on label sets and a coinductive LTS for global types, then proves Subject Reduction and Session Fidelity for the resulting type system. Lock-Freedom and Orphan-Message-Freedom are derived consequences of those theorems. No step reduces a claimed result to a fitted parameter, a self-referential equation, or a load-bearing self-citation; the coherence definition is an orthogonal syntactic condition whose interaction with the LTS is established by explicit proof rather than by construction. This is standard, self-contained formal development.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claims rest on standard mathematical machinery (coinduction) and a domain-specific coherence predicate; no free parameters or invented entities are introduced.

axioms (2)

standard math Coinductively defined labelled transition system on global types
Basis for the type system and transition semantics.
domain assumption Coherence of sets of communication labels
Defined roughly as containing all enabled communications or all actions of a participant with the input condition; used to type sessions.

pith-pipeline@v0.9.0 · 5490 in / 1374 out tokens · 48715 ms · 2026-05-10T17:06:05.103296+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

28 extracted references · 28 canonical work pages

[1]

Journal of Logical and Algebraic Methods in Programming 144, p

Franco Barbanera, Viviana Bono & Mariangiola Dezani-Ci ancaglini (2025): Open compliance in multiparty sessions with partial typing . Journal of Logical and Algebraic Methods in Programming 144, p. 101046, doi:10.1016/j.jlamp.2025.101046

work page doi:10.1016/j.jlamp.2025.101046 2025
[2]

Available at https://github.com/ francobarbanera/Asynchronous-Multiparty-Sessions-wi th-Mixed-Choice-Full/blob/ b68cd679b435d0ac1f12e9c8ab47cc8167a11728/Main-Mix-A sync-full.pdf

Franco Barbanera & Mariangiola Dezani: Asynchronous Multiparty Ses- sions with Mixed Choice (full version) . Available at https://github.com/ francobarbanera/Asynchronous-Multiparty-Sessions-wi th-Mixed-Choice-Full/blob/ b68cd679b435d0ac1f12e9c8ab47cc8167a11728/Main-Mix-A sync-full.pdf

work page
[3]

In Tiziana Margaria & Bernhard Steffen, editors: Essays Dedicated to Rocco De Nicola on The Occasion of His 70th Birthday , LNCS 15219, Springer, pp

Franco Barbanera & Mariangiola Dezani-Ciancaglini (20 24): Asynchronous Multiparty Sessions with In- ternal Delegation . In Tiziana Margaria & Bernhard Steffen, editors: Essays Dedicated to Rocco De Nicola on The Occasion of His 70th Birthday , LNCS 15219, Springer, pp. 322–339, doi: 10.1007/ 978-3-031-73709-1_20

work page
[4]

In Cl´ ement Aubert, Cinzia Di Giusto, Simon Fowler & Violet Ka I Pun, editors: ICE, EPTCS 425, pp

Franco Barbanera & Mariangiola Dezani-Ciancaglini (20 25): Modular Multiparty Sessions with Mixed Choice. In Cl´ ement Aubert, Cinzia Di Giusto, Simon Fowler & Violet Ka I Pun, editors: ICE, EPTCS 425, pp. 2–20, doi: 10.4204/EPTCS.425.2

work page doi:10.4204/eptcs.425.2
[5]

In Sandra Alves & Ian Mackie, editors: DCM, EPTCS 408, Open Publishing Association, pp

Franco Barbanera, Mariangiola Dezani-Ciancaglini & Ug o de’Liguoro (2024): Partial Typing for Asyn- chronous Multiparty Sessions. In Sandra Alves & Ian Mackie, editors: DCM, EPTCS 408, Open Publishing Association, pp. 1–20, doi: 10.4204/EPTCS.408.1

work page doi:10.4204/eptcs.408.1 2024
[6]

In Alessandro Bruni, Alberto Momigliano, Matteo Pradella & Matteo Rossi, editors: PPDP, ACM Press, pp

Franco Barbanera, Mariangiola Dezani-Ciancaglini & Ug o de’Liguoro (2024): Un-projectable Global Types for Multiparty Sessions. In Alessandro Bruni, Alberto Momigliano, Matteo Pradella & Matteo Rossi, editors: PPDP, ACM Press, pp. 15:1–15:13, doi: 10.1145/3678232.3678245

work page doi:10.1145/3678232.3678245 2024
[7]

[CS09] Bernadette Charron-Bost and Andr´ e Schiper

Daniel Brand & Pitro Zaﬁropulo (1983): On Communicating Finite-state Machines . Journal of the ACM 30(2), pp. 323–342, doi: 10.1145/322374.322380

work page doi:10.1145/322374.322380 1983
[8]

V asconcelos (20 22): Mixed sessions

Filipe Casal, Andreia Mordido & V asco T. V asconcelos (20 22): Mixed Sessions . Theoretical Computer Science 897, pp. 23–48, doi: 10.1016/J.TCS.2021.08.005

work page doi:10.1016/j.tcs.2021.08.005 2021
[9]

ACM Program

David Castro-Perez, Francisco Ferreira & Sung-Shik Jon gmans (2026): A Synthetic Reconstruction of Mul- tiparty Session Types. ACM Program. Lang. 10(POPL), pp. 1442–1470, doi: 10.1145/3776692

work page doi:10.1145/3776692 2026
[10]

Information and Computation 202(2), pp

G´ erard C´ ec´ e & Alain Finkel (2005):V eriﬁcation of Programs with Half-duplex Communication. Information and Computation 202(2), pp. 166–190, doi: 10.1016/J.IC.2005.05.006

work page doi:10.1016/j.ic.2005.05.006 2005
[11]

Logical Methods in Computer Science 19(1), pp

Francesco Dagnino, Paola Giannini & Mariangiola Dezan i-Ciancaglini (2023): Deconﬁned Global Types for Asynchronous Sessions. Logical Methods in Computer Science 19(1), pp. 1–41, doi:10.46298/lmcs-19(1: 3)2023

work page doi:10.46298/lmcs-19(1: 2023
[12]

In Helmut Seidl, editor: ESOP, LNCS 7211, Springer, pp

Pierre-Malo Deni´ elou & Nobuko Y oshida (2012):Multiparty Session Types Meet Communicating Automata. In Helmut Seidl, editor: ESOP, LNCS 7211, Springer, pp. 194–213, doi: 10.1007/978-3-642-28869-2_ 10

work page doi:10.1007/978-3-642-28869-2_ 2012
[13]

In Fedor V

Pierre-Malo Deni´ elou & Nobuko Y oshida (2013): Multiparty Compatibility in Communicating Automata: Characterisation and Synthesis of Global Session Types . In Fedor V . Fomin, Rusins Freivalds, Marta Z. Kwiatkowska & David Peleg, editors: ICALP, LNCS 7966, Springer, pp. 174–186, doi: 10.1007/ 978-3-642-39212-2_18

work page 2013
[14]

Gouda, Eric G

Mohamed G. Gouda, Eric G. Manning & Y ao-Tin Y u (1984): On the Progress of Communication Between Two Machines. Information and Control 63(3), pp. 200–2016, doi: 10.1016/S0019-9958(84)80014-5

work page doi:10.1016/s0019-9958(84)80014-5 1984
[15]

In George C

Kohei Honda, Nobuko Y oshida & Marco Carbone (2008): Multiparty Asynchronous Session Types . In George C. Necula & Philip Wadler, editors: POPL, ACM Press, pp. 273–284, doi: 10.1145/1328897. 1328472

work page doi:10.1145/1328897 2008
[16]

doi:10.1145/2827695

Kohei Honda, Nobuko Y oshida & Marco Carbone (2016): Multiparty Asynchronous Session Types. Journal of the ACM 63(1), pp. 9:1–9:67, doi: 10.1145/2827695. 22 Asynchronous Multiparty Sessions with Mixed Choice

work page doi:10.1145/2827695 2016
[17]

Mathematical Structures in Computer Science 27(7), pp

Dexter Kozen & Alexandra Silva (2017): Practical Coinduction . Mathematical Structures in Computer Science 27(7), pp. 1132–1152, doi: 10.1017/S0960129515000493

work page doi:10.1017/s0960129515000493 2017
[18]

In Isil Dillig & Serdar Tasiran, editors: CA V, LNCS 11561, Springer, pp

Julien Lange & Nobuko Y oshida (2019): V erifying Asynchronous Interactions via Communicating Se ssion Automata. In Isil Dillig & Serdar Tasiran, editors: CA V, LNCS 11561, Springer, pp. 97–117, doi: 10.1007/ 978-3-030-25540-4_6

work page 2019
[19]

In Serge Haddad & Daniele V aracca, editors: CONCUR, LIPIcs 203, Schloss Dagstuhl, pp

Rupak Majumdar, Madhavan Mukund, Felix Stutz & Damien Z ufferey (2021): Generalising projection in asynchronous multiparty session types. In Serge Haddad & Daniele V aracca, editors: CONCUR, LIPIcs 203, Schloss Dagstuhl, pp. 35:1–35:24, doi: 10.4230/LIPIcs.CONCUR.2021.35

work page doi:10.4230/lipics.concur.2021.35 2021
[20]

In Kathrin Stark, Y annick Zakowski, Nikhil Swamy & Nicolas Tabareau, editors: CPP, ACM, pp

Virgil Marionneau, F´ elix Sassus Bourda, Alejandro Aguirre & Lars Birkedal (2026): Modular Speciﬁcations and Implementations of Random Samplers in Higher-Order Sep aration Logic . In Kathrin Stark, Y annick Zakowski, Nikhil Swamy & Nicolas Tabareau, editors: CPP, ACM, pp. 368–382, doi: 10.1145/3779031. 3779109

work page doi:10.1145/3779031 2026
[21]

In Thomas A

Luca Padovani (2014): Deadlock and Lock Freedom in the Linear π-Calculus. In Thomas A. Henzinger & Dale Miller, editors: CSL-LICS, ACM Press, pp. 72:1–72:10, doi: 10.1007/978-3-662-43376-8_10

work page doi:10.1007/978-3-662-43376-8_10 2014
[22]

In Sung-Shik Jongmans & Ant´ onia Lopes, editors:COORDINA TION, LNCS 13908, Springer, pp

Jonah Pears, Laura Bocchi & Andy King (2023): Safe Asynchronous Mixed-Choice for Timed Interactions . In Sung-Shik Jongmans & Ant´ onia Lopes, editors:COORDINA TION, LNCS 13908, Springer, pp. 214–231, doi:10.1007/978-3-031-35361-1_12

work page doi:10.1007/978-3-031-35361-1_12 2023
[23]

Logical Methods in Computer Science 21(3), doi:10.46298/LMCS-21(3:6)2025

Jonah Pears, Laura Bocchi, Maurizio Murgia & Andy King ( 2025): Timeout Asynchronous Session Types: Safe Asynchronous Mixed-Choice F or Timed Interactions . Logical Methods in Computer Science 21(3), doi:10.46298/LMCS-21(3:6)2025

work page doi:10.46298/lmcs-21(3:6)2025 2025
[24]

Information and Computation 298, p

Kirstin Peters & Nobuko Y oshida (2024): Mixed Choice in Session Types. Information and Computation 298, p. 105164, doi: 10.1016/J.IC.2024.105164

work page doi:10.1016/j.ic.2024.105164 2024
[25]

Injective hardness condition for PCSPs

Kirstin Peters & Nobuko Y oshida (2024): Separation and Encodability in Mixed Choice Multiparty Ses sions. In Pawel Sobocinski, Ugo Dal Lago & Javier Esparza, editors: LICS, ACM Press, pp. 62:1–62:15, doi: 10. 1145/3661814.3662085

work page arXiv 2024
[26]

Pierce (2002): Types and Programming Languages

Benjamin C. Pierce (2002): Types and Programming Languages. MIT Press

work page 2002
[27]

Less is more: multiparty session ty pes revisited

Alceste Scalas & Nobuko Y oshida (2019): Less is More: Multiparty Session Types Revisited . P ACMPL 3 (POPL), pp. 30:1–30:29, doi: 10.1145/3290343

work page doi:10.1145/3290343 2019
[28]

In Viktor V afeiadis, editor: ESOP, LNCS 15695, Springer, pp

Felix Stutz & Emanuele D’Osualdo (2025): An Automata-theoretic Basis for Speciﬁcation and Type Checking of Multiparty Protocols . In Viktor V afeiadis, editor: ESOP, LNCS 15695, Springer, pp. 314–346, doi: 10. 1007/978-3-031-91121-7_13

work page 2025

[1] [1]

Journal of Logical and Algebraic Methods in Programming 144, p

Franco Barbanera, Viviana Bono & Mariangiola Dezani-Ci ancaglini (2025): Open compliance in multiparty sessions with partial typing . Journal of Logical and Algebraic Methods in Programming 144, p. 101046, doi:10.1016/j.jlamp.2025.101046

work page doi:10.1016/j.jlamp.2025.101046 2025

[2] [2]

Available at https://github.com/ francobarbanera/Asynchronous-Multiparty-Sessions-wi th-Mixed-Choice-Full/blob/ b68cd679b435d0ac1f12e9c8ab47cc8167a11728/Main-Mix-A sync-full.pdf

Franco Barbanera & Mariangiola Dezani: Asynchronous Multiparty Ses- sions with Mixed Choice (full version) . Available at https://github.com/ francobarbanera/Asynchronous-Multiparty-Sessions-wi th-Mixed-Choice-Full/blob/ b68cd679b435d0ac1f12e9c8ab47cc8167a11728/Main-Mix-A sync-full.pdf

work page

[3] [3]

In Tiziana Margaria & Bernhard Steffen, editors: Essays Dedicated to Rocco De Nicola on The Occasion of His 70th Birthday , LNCS 15219, Springer, pp

Franco Barbanera & Mariangiola Dezani-Ciancaglini (20 24): Asynchronous Multiparty Sessions with In- ternal Delegation . In Tiziana Margaria & Bernhard Steffen, editors: Essays Dedicated to Rocco De Nicola on The Occasion of His 70th Birthday , LNCS 15219, Springer, pp. 322–339, doi: 10.1007/ 978-3-031-73709-1_20

work page

[4] [4]

In Cl´ ement Aubert, Cinzia Di Giusto, Simon Fowler & Violet Ka I Pun, editors: ICE, EPTCS 425, pp

Franco Barbanera & Mariangiola Dezani-Ciancaglini (20 25): Modular Multiparty Sessions with Mixed Choice. In Cl´ ement Aubert, Cinzia Di Giusto, Simon Fowler & Violet Ka I Pun, editors: ICE, EPTCS 425, pp. 2–20, doi: 10.4204/EPTCS.425.2

work page doi:10.4204/eptcs.425.2

[5] [5]

In Sandra Alves & Ian Mackie, editors: DCM, EPTCS 408, Open Publishing Association, pp

Franco Barbanera, Mariangiola Dezani-Ciancaglini & Ug o de’Liguoro (2024): Partial Typing for Asyn- chronous Multiparty Sessions. In Sandra Alves & Ian Mackie, editors: DCM, EPTCS 408, Open Publishing Association, pp. 1–20, doi: 10.4204/EPTCS.408.1

work page doi:10.4204/eptcs.408.1 2024

[6] [6]

In Alessandro Bruni, Alberto Momigliano, Matteo Pradella & Matteo Rossi, editors: PPDP, ACM Press, pp

Franco Barbanera, Mariangiola Dezani-Ciancaglini & Ug o de’Liguoro (2024): Un-projectable Global Types for Multiparty Sessions. In Alessandro Bruni, Alberto Momigliano, Matteo Pradella & Matteo Rossi, editors: PPDP, ACM Press, pp. 15:1–15:13, doi: 10.1145/3678232.3678245

work page doi:10.1145/3678232.3678245 2024

[7] [7]

[CS09] Bernadette Charron-Bost and Andr´ e Schiper

Daniel Brand & Pitro Zaﬁropulo (1983): On Communicating Finite-state Machines . Journal of the ACM 30(2), pp. 323–342, doi: 10.1145/322374.322380

work page doi:10.1145/322374.322380 1983

[8] [8]

V asconcelos (20 22): Mixed sessions

Filipe Casal, Andreia Mordido & V asco T. V asconcelos (20 22): Mixed Sessions . Theoretical Computer Science 897, pp. 23–48, doi: 10.1016/J.TCS.2021.08.005

work page doi:10.1016/j.tcs.2021.08.005 2021

[9] [9]

ACM Program

David Castro-Perez, Francisco Ferreira & Sung-Shik Jon gmans (2026): A Synthetic Reconstruction of Mul- tiparty Session Types. ACM Program. Lang. 10(POPL), pp. 1442–1470, doi: 10.1145/3776692

work page doi:10.1145/3776692 2026

[10] [10]

Information and Computation 202(2), pp

G´ erard C´ ec´ e & Alain Finkel (2005):V eriﬁcation of Programs with Half-duplex Communication. Information and Computation 202(2), pp. 166–190, doi: 10.1016/J.IC.2005.05.006

work page doi:10.1016/j.ic.2005.05.006 2005

[11] [11]

Logical Methods in Computer Science 19(1), pp

Francesco Dagnino, Paola Giannini & Mariangiola Dezan i-Ciancaglini (2023): Deconﬁned Global Types for Asynchronous Sessions. Logical Methods in Computer Science 19(1), pp. 1–41, doi:10.46298/lmcs-19(1: 3)2023

work page doi:10.46298/lmcs-19(1: 2023

[12] [12]

In Helmut Seidl, editor: ESOP, LNCS 7211, Springer, pp

Pierre-Malo Deni´ elou & Nobuko Y oshida (2012):Multiparty Session Types Meet Communicating Automata. In Helmut Seidl, editor: ESOP, LNCS 7211, Springer, pp. 194–213, doi: 10.1007/978-3-642-28869-2_ 10

work page doi:10.1007/978-3-642-28869-2_ 2012

[13] [13]

In Fedor V

Pierre-Malo Deni´ elou & Nobuko Y oshida (2013): Multiparty Compatibility in Communicating Automata: Characterisation and Synthesis of Global Session Types . In Fedor V . Fomin, Rusins Freivalds, Marta Z. Kwiatkowska & David Peleg, editors: ICALP, LNCS 7966, Springer, pp. 174–186, doi: 10.1007/ 978-3-642-39212-2_18

work page 2013

[14] [14]

Gouda, Eric G

Mohamed G. Gouda, Eric G. Manning & Y ao-Tin Y u (1984): On the Progress of Communication Between Two Machines. Information and Control 63(3), pp. 200–2016, doi: 10.1016/S0019-9958(84)80014-5

work page doi:10.1016/s0019-9958(84)80014-5 1984

[15] [15]

In George C

Kohei Honda, Nobuko Y oshida & Marco Carbone (2008): Multiparty Asynchronous Session Types . In George C. Necula & Philip Wadler, editors: POPL, ACM Press, pp. 273–284, doi: 10.1145/1328897. 1328472

work page doi:10.1145/1328897 2008

[16] [16]

doi:10.1145/2827695

Kohei Honda, Nobuko Y oshida & Marco Carbone (2016): Multiparty Asynchronous Session Types. Journal of the ACM 63(1), pp. 9:1–9:67, doi: 10.1145/2827695. 22 Asynchronous Multiparty Sessions with Mixed Choice

work page doi:10.1145/2827695 2016

[17] [17]

Mathematical Structures in Computer Science 27(7), pp

Dexter Kozen & Alexandra Silva (2017): Practical Coinduction . Mathematical Structures in Computer Science 27(7), pp. 1132–1152, doi: 10.1017/S0960129515000493

work page doi:10.1017/s0960129515000493 2017

[18] [18]

In Isil Dillig & Serdar Tasiran, editors: CA V, LNCS 11561, Springer, pp

Julien Lange & Nobuko Y oshida (2019): V erifying Asynchronous Interactions via Communicating Se ssion Automata. In Isil Dillig & Serdar Tasiran, editors: CA V, LNCS 11561, Springer, pp. 97–117, doi: 10.1007/ 978-3-030-25540-4_6

work page 2019

[19] [19]

In Serge Haddad & Daniele V aracca, editors: CONCUR, LIPIcs 203, Schloss Dagstuhl, pp

Rupak Majumdar, Madhavan Mukund, Felix Stutz & Damien Z ufferey (2021): Generalising projection in asynchronous multiparty session types. In Serge Haddad & Daniele V aracca, editors: CONCUR, LIPIcs 203, Schloss Dagstuhl, pp. 35:1–35:24, doi: 10.4230/LIPIcs.CONCUR.2021.35

work page doi:10.4230/lipics.concur.2021.35 2021

[20] [20]

In Kathrin Stark, Y annick Zakowski, Nikhil Swamy & Nicolas Tabareau, editors: CPP, ACM, pp

Virgil Marionneau, F´ elix Sassus Bourda, Alejandro Aguirre & Lars Birkedal (2026): Modular Speciﬁcations and Implementations of Random Samplers in Higher-Order Sep aration Logic . In Kathrin Stark, Y annick Zakowski, Nikhil Swamy & Nicolas Tabareau, editors: CPP, ACM, pp. 368–382, doi: 10.1145/3779031. 3779109

work page doi:10.1145/3779031 2026

[21] [21]

In Thomas A

Luca Padovani (2014): Deadlock and Lock Freedom in the Linear π-Calculus. In Thomas A. Henzinger & Dale Miller, editors: CSL-LICS, ACM Press, pp. 72:1–72:10, doi: 10.1007/978-3-662-43376-8_10

work page doi:10.1007/978-3-662-43376-8_10 2014

[22] [22]

In Sung-Shik Jongmans & Ant´ onia Lopes, editors:COORDINA TION, LNCS 13908, Springer, pp

Jonah Pears, Laura Bocchi & Andy King (2023): Safe Asynchronous Mixed-Choice for Timed Interactions . In Sung-Shik Jongmans & Ant´ onia Lopes, editors:COORDINA TION, LNCS 13908, Springer, pp. 214–231, doi:10.1007/978-3-031-35361-1_12

work page doi:10.1007/978-3-031-35361-1_12 2023

[23] [23]

Logical Methods in Computer Science 21(3), doi:10.46298/LMCS-21(3:6)2025

Jonah Pears, Laura Bocchi, Maurizio Murgia & Andy King ( 2025): Timeout Asynchronous Session Types: Safe Asynchronous Mixed-Choice F or Timed Interactions . Logical Methods in Computer Science 21(3), doi:10.46298/LMCS-21(3:6)2025

work page doi:10.46298/lmcs-21(3:6)2025 2025

[24] [24]

Information and Computation 298, p

Kirstin Peters & Nobuko Y oshida (2024): Mixed Choice in Session Types. Information and Computation 298, p. 105164, doi: 10.1016/J.IC.2024.105164

work page doi:10.1016/j.ic.2024.105164 2024

[25] [25]

Injective hardness condition for PCSPs

Kirstin Peters & Nobuko Y oshida (2024): Separation and Encodability in Mixed Choice Multiparty Ses sions. In Pawel Sobocinski, Ugo Dal Lago & Javier Esparza, editors: LICS, ACM Press, pp. 62:1–62:15, doi: 10. 1145/3661814.3662085

work page arXiv 2024

[26] [26]

Pierce (2002): Types and Programming Languages

Benjamin C. Pierce (2002): Types and Programming Languages. MIT Press

work page 2002

[27] [27]

Less is more: multiparty session ty pes revisited

Alceste Scalas & Nobuko Y oshida (2019): Less is More: Multiparty Session Types Revisited . P ACMPL 3 (POPL), pp. 30:1–30:29, doi: 10.1145/3290343

work page doi:10.1145/3290343 2019

[28] [28]

In Viktor V afeiadis, editor: ESOP, LNCS 15695, Springer, pp

Felix Stutz & Emanuele D’Osualdo (2025): An Automata-theoretic Basis for Speciﬁcation and Type Checking of Multiparty Protocols . In Viktor V afeiadis, editor: ESOP, LNCS 15695, Springer, pp. 314–346, doi: 10. 1007/978-3-031-91121-7_13

work page 2025