一句话：提出支持异步混合选择的多参与者会话类型框架，允许协议状态瞬时不一致但保证最终一致，并实现工具链与 Erlang 案例。
本文针对异步多参与者会话类型（MST）中混合选择（参与者既能发送又能接收的选择）难以处理的问题，提出一个支持异步混合选择（MC）的 MST 框架。作者设计了一个 MC 核心构造，允许分布式参与者之间的协议状态出现瞬时不一致，但保证所有参与者最终总能到达相互一致的状态。为验证系统正确性，作者建立了进展性（progress）性质，并证明了全局类型与其分布式局部类型投影之间的操作对应关系。基于该理论，作者实现了一个用于规约和验证含 MC 的异步 MST 协议的工具链，并可在 Erlang/OTP 中编写符合规范的 gen_statem 进程。最后，作者使用该工具链重新实现了 RabbitMQ broker 的 Erlang amqp_client 的一部分，以检验框架的实用性。
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.
@article{paperbot3793,
title = {Mixed Choice in Asynchronous Multiparty Session Types},
author = {Laura Bocchi and Raymond Hu and Adriana Laura Voinea and Simon Thompson},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA1},
year = {2026},
doi = {10.1145/3798256}
}