Mixed Choice in Asynchronous Multiparty Session Types

Laura Bocchi; RAYMOND HU; Adriana Laura Voinea; Simon Thompson

doi:10.1145/3798256

journal article Apr 10, 2026

Mixed Choice in Asynchronous Multiparty Session Types

Laura Bocchi

RAYMOND HU

Adriana Laura Voinea

Simon Thompson

Proceedings of the ACM on Programming Languages Vol. 10 No. OOPSLA1 pp. 1542-1569 · Association for Computing Machinery (ACM)

View at Publisher Save 10.1145/3798256

Abstract

We present a multiparty session type (MST) framework with
asynchronous mixed choice
(MC). We propose a core construct for MC that allows transient inconsistencies in protocol state between distributed participants, but ensures all participants can always eventually reach a mutually consistent state. We prove the correctness of our system by establishing a progress property and an operational correspondence between global types and distributed local type projections. Based on our theory, we implement a practical toolchain for specifying and validating asynchronous MST protocols featuring MC, and programming compliant gen_statem processes in Erlang/OTP. We test our framework by using our toolchain to specify and reimplement part of the amqp_client of the RabbitMQ broker for Erlang.

Topics

No keywords indexed for this article. Browse by subject →

References

49

[1]

Manuel Adameit, Kirstin Peters, and Uwe Nestmann. 2017. Session Types for Link Failures. In FORTE (Lecture Notes in Computer Science, Vol. 10321). Springer, 1–16.

[2]

10.4230/lipics.ecoop.2023.1

[3]

10.4230/lipics.concur.2022.35

[4]

Lorenzo Bettini, Mario Coppo, Loris D’Antoni, Marco De Luca, Mariangiola Dezani-Ciancaglini, and Nobuko Yoshida. 2008. Global Progress in Dynamically Interleaved Multiparty Sessions. In CONCUR (LNCS, Vol. 5201). 418–433. isbn:978-3-540-85360-2

[5]

10.48550/arxiv.2602.23927

[6]

10.5281/zenodo.18808387

[7]

10.1145/322374.322380

[8]

10.1007/978-3-031-62645-6_6

[9]

10.1017/s0960129514000218

[10]

10.1017/s0960129514000164

[11]

10.1007/978-3-540-85361-9_32

[12]

10.4204/eptcs.314.5

[13]

10.1016/j.tcs.2021.08.005

[14]

10.2168/lmcs-8(1:24)2012

[15]

10.23638/lmcs-13(2:12)2017

[16]

10.1007/978-3-319-39570-8_7

[17]

10.1016/j.jlamp.2024.100964

[18]

10.1007/978-3-319-18941-3_4

[19]

10.1017/s0960129514000188

[20]

10.1007/s10703-014-0218-8

[21]

Pierre-Malo Deniélou and Nobuko Yoshida. 2012. Multiparty Session Types Meet Communicating Automata. In ESOP (LNCS, Vol. 7211). 194–213.

[22]

Pierre-Malo Deniélou and Nobuko Yoshida. 2013. Multiparty Compatibility in Communicating Automata: Characterisation and Synthesis of Global Session Types. In ICALP (LNCS, Vol. 7966). 174–186.

[23]

10.1145/3290341

[24]

10.1016/s0019-9958(84)80014-5

[25]

10.1145/1328438.1328472

[26]

10.1145/2827695

[27]

10.4230/lipics.ecoop.2024.19

[28]

10.1007/978-3-642-14107-2_16

[29]

10.1007/978-3-662-49665-7_24

[30]

Foundations of Session Types and Behavioural Contracts

Hans Hüttel, Ivan Lanese, Vasco T. Vasconcelos et al.

ACM Computing Surveys 10.1145/2873052

[31]

10.1145/3622854

[32]

10.4230/lipics.ecoop.2023.42

[33]

10.1007/978-3-030-44914-8_10

[34]

10.1145/3180155.3180157

[35]

10.1007/978-3-030-25540-4_6

[36]

10.1007/978-3-031-37709-9_17

[37]

10.4230/lipics.concur.2021.35

[38]

10.4230/lipics.ecoop.2025.24

[39]

10.1007/978-3-031-35361-1_12

[40]

10.46298/lmcs-19(4:14)2023

[41]

10.48550/arxiv.2405.08104

[42]

10.1145/3290343

[43]

10.4230/lipics.ecoop.2023.32

[44]

10.48550/arxiv.2501.16977

[45]

10.1007/978-3-030-44914-8_26

[46]

10.1007/978-3-319-89884-1_28

[47]

10.1145/3485501

[48]

10.1017/s095679681400001x

[49]

10.1007/978-3-319-05119-2_3

Metrics

0

Citations

49

References

Details

Published: Apr 10, 2026
Vol/Issue: 10(OOPSLA1)
Pages: 1542-1569

Authors

L

Laura Bocchi

University of Kent, Canterbury, United Kingdom

R

RAYMOND HU

Queen Mary University of London, London, United Kingdom

A

Adriana Laura Voinea

University of Glasgow, Glasgow, United Kingdom

S

Simon Thompson

University of Kent, Canterbury, United Kingdom

Funding

EPSRC Award: EP/T014512/1

Cite This Article

Laura Bocchi, RAYMOND HU, Adriana Laura Voinea, et al. (2026). Mixed Choice in Asynchronous Multiparty Session Types. Proceedings of the ACM on Programming Languages, 10(OOPSLA1), 1542-1569. https://doi.org/10.1145/3798256

Mixed Choice in Asynchronous Multiparty Session Types

You May Also Like