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.

翻译：我们提出了一种支持异步混合选择（MC）的多参与者会话类型（MST）框架。我们设计了一个核心结构来实现MC，该结构允许分布式参与者之间的协议状态存在暂时不一致，但确保所有参与者最终总能达到相互一致的状态。我们通过建立进展性质以及全局类型与分布式局部类型投影之间的操作对应关系，证明了系统的正确性。基于我们的理论，我们实现了一个实用的工具链，用于规范和验证支持MC的异步MST协议，并在Erlang/OTP中编程符合规范的gen_statem进程。我们通过使用该工具链来规范和重新实现RabbitMQ代理中用于Erlang的amqp_client部分，从而测试了我们的框架。