Paper
Mixed Choice in Asynchronous Multiparty Session Types
Authors
Laura Bocchi, Raymond Hu, Adriana Laura Voinea, Simon Thompson
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.
Metadata
Related papers
Fractal universe and quantum gravity made simple
Fabio Briscese, Gianluca Calcagni • 2026-03-25
POLY-SIM: Polyglot Speaker Identification with Missing Modality Grand Challenge 2026 Evaluation Plan
Marta Moscati, Muhammad Saad Saeed, Marina Zanoni, Mubashir Noman, Rohan Kuma... • 2026-03-25
LensWalk: Agentic Video Understanding by Planning How You See in Videos
Keliang Li, Yansong Li, Hongze Shen, Mengdi Liu, Hong Chang, Shiguang Shan • 2026-03-25
Orientation Reconstruction of Proteins using Coulomb Explosions
Tomas André, Alfredo Bellisario, Nicusor Timneanu, Carl Caleman • 2026-03-25
The role of spatial context and multitask learning in the detection of organic and conventional farming systems based on Sentinel-2 time series
Jan Hemmerling, Marcel Schwieder, Philippe Rufin, Leon-Friedrich Thomas, Mire... • 2026-03-25
Raw Data (Debug)
{
"raw_xml": "<entry>\n <id>http://arxiv.org/abs/2602.23927v1</id>\n <title>Mixed Choice in Asynchronous Multiparty Session Types</title>\n <updated>2026-02-27T11:21:58Z</updated>\n <link href='https://arxiv.org/abs/2602.23927v1' rel='alternate' type='text/html'/>\n <link href='https://arxiv.org/pdf/2602.23927v1' rel='related' title='pdf' type='application/pdf'/>\n <summary>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.</summary>\n <category scheme='http://arxiv.org/schemas/atom' term='cs.DC'/>\n <category scheme='http://arxiv.org/schemas/atom' term='cs.FL'/>\n <category scheme='http://arxiv.org/schemas/atom' term='cs.MA'/>\n <category scheme='http://arxiv.org/schemas/atom' term='cs.PL'/>\n <category scheme='http://arxiv.org/schemas/atom' term='cs.SE'/>\n <published>2026-02-27T11:21:58Z</published>\n <arxiv:primary_category term='cs.DC'/>\n <author>\n <name>Laura Bocchi</name>\n </author>\n <author>\n <name>Raymond Hu</name>\n </author>\n <author>\n <name>Adriana Laura Voinea</name>\n </author>\n <author>\n <name>Simon Thompson</name>\n </author>\n </entry>"
}