一句话：提出首个混合选择多方消息传递的高阶分离逻辑 Mixtris，并在 Rocq/Iris 中机械验证其可靠性与实例。
混合选择多方消息传递允许组件通过非确定性在并发发送和接收选项间选择，能简洁表达领导者选举等高级算法，但此前缺乏程序逻辑。本文提出 Mixtris，一个用于共享内存设置下、带混合选择多方消息传递的高阶命令式程序功能正确性推理的机械化高阶分离逻辑。Mixtris 借鉴混合选择多方消息传递的会话类型系统，扩展现有非混合选择多方消息传递分离逻辑，并首次为该范式建立程序逻辑。作者提出新的混合选择多方协议模型以证明 Mixtris 的可靠性。所有元理论和示例均在 Rocq 证明助手上的 Iris 框架中形式化，包括 Chang 和 Roberts 的环领导者选举协议等挑战性例子。
Mixed choice multiparty message passing is an expressive concurrency programming paradigm where components use non-determinism to choose between concurrent options for sending and receiving messages. This flexibility makes it possible to program advanced algorithms, such as leader election protocols, succinctly. We present Mixtris, a mechanised higher-order separation logic for reasoning about functional correctness of higher-order imperative programs with mixed choice multiparty message passing in a shared memory setting. Mixtris builds upon recent work on separation logic for (non-mixed choice) multiparty message-passing programs, by drawing inspiration from session type systems for mixed choice multiparty message-passing programs. Mixtris is the first program logic for mixed choice multiparty message passing. We prove soundness of Mixtris using a novel model of our mixed choice multiparty protocols. We demonstrate how Mixtris can be used to formally reason about challenging examples, including some leader election protocols such as Chang and Roberts’s ring leader election protocol. All the results in the paper (both meta-theory and examples) have been formalised in the Rocq proof assistant on top of the Iris program logic framework.
@article{paperbot3803,
title = {Mixtris: Mechanised Higher-Order Separation Logic for Mixed Choice Multiparty Message Passing},
author = {Jonas Kastberg Hinrichsen and Iwan Quémerais and Lars Birkedal},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA1},
year = {2026},
doi = {10.1145/3798224}
}