AI 中文总结
该研究将状态变换子模型引入编排编程，在Lean中机械化实现支持多种通信与方法的编排语言，证明了端点投影等性质及霍尔逻辑，规避了绑定替换问题以简化机械化。
AI 中文摘要
编排编程是一种用于开发分布式应用的编程模型，它将整个通信协议编写为单个程序，再由编译器将其投影到每个参与方对应的进程中。编排编程抽象了套接字等底层网络通信原语，且通过构造确保无死锁，提供了高度的安全性保证。编排的机械化必然要处理分布式编程特有的操作、非分布式程序中也存在的标准（局部）操作，以及绑定和替换这类典型问题。我们旨在规避后一类问题，从而获得更简洁的机械化实现，聚焦于编排的核心分布式方面。为此，我们采用Thiemann近期提出的方法，在依赖类型语言中优雅地为无死锁进程建模：使用状态变换子表示每个进程执行的计算。我们将状态变换子模型引入编排，减少了绑定和替换相关的常规机械化工作量，并对语言的“局部”方面细节进行抽象。我们在Lean中实现了对编排语言的机械化，该语言支持点对点通信、广播、递归过程和局部有状态方法，允许为每个参与方分配不同的方法集。我们证明了端点投影的正确性与完备性，确立了投影进程的无死锁性，证明了合流性，并验证了编排的霍尔逻辑。
英文摘要
Choreographic programming is a programming model for developing distributed applications where an entire communication protocol is written as a single program, which a compiler then projects to one process per participant. Choreographic programming abstracts over low-level network communication primitives such as sockets, and provides a high degree of safety guarantees with deadlock freedom ensured by construction. Mechanizing choreographies necessarily deals with both operations specific to distributed programming and standard (local) operations that also occur in non-distributed programs, as well as the typical issues of binding and substitution. We aim to sidestep the latter issues, thereby obtaining a more concise mechanization that focuses on the essential distributed aspects of choreographies. To this end, we use a method recently proposed by Thiemann to elegantly model deadlock-free processes in a dependently typed language: Using state transformers to represent the computations performed by each process. We bring the state transformer model to choreographies, allowing us to reduce the usual mechanization effort around binding and substitution, and to abstract over the details of the "local" aspects of the language. We mechanize in Lean a choreographic language that supports point-to-point communication, broadcasting, recursive procedures, and local stateful methods, allowing each participant to be assigned a different set of methods. We prove soundness and completeness of endpoint projection, establish deadlock freedom for the projected processes, prove confluence, and verify a Hoare logic for choreographies.
CommentsTo be published in the TyDe 2026 proceedings
