Mixed Choice in Asynchronous Multiparty Session Types
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2026
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866910035204898816 |
|---|---|
| author | Bocchi, Laura Hu, Raymond Voinea, Adriana Laura Thompson, Simon |
| author_facet | Bocchi, Laura Hu, Raymond Voinea, Adriana Laura Thompson, Simon |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2602_23927 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Mixed Choice in Asynchronous Multiparty Session Types Bocchi, Laura Hu, Raymond Voinea, Adriana Laura Thompson, Simon Distributed, Parallel, and Cluster Computing Formal Languages and Automata Theory Multiagent Systems Programming Languages Software Engineering 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. |
| title | Mixed Choice in Asynchronous Multiparty Session Types |
| topic | Distributed, Parallel, and Cluster Computing Formal Languages and Automata Theory Multiagent Systems Programming Languages Software Engineering |
| url | https://arxiv.org/abs/2602.23927 |