Mech：机械化编排编程
Mech: Mechanised Choreographic Programming
AI总结：
研究针对编排编程，提出在Lean 4中的新机械化Mech，解决现有问题。核心方法是制定新语义、揭示代数定律。主要贡献是证明EPP相关特性，推导投影网络相关属性，形成最广泛的CP机械化理论。
AI中文摘要：
编排编程（CP）是一种用于并发和分布式系统构造正确开发的编程范式。程序员从全局视角编写系统预期的整体行为编排，然后通过端点投影（EPP）自动编译为通信端点程序。对于有表现力的CP语言，实现这一承诺变得微妙。现有CP机械化仅处理受限片段，教科书和具有丰富特性的通用语言实现使关键交互不规范。我们提出了Mech，一种在Lean 4中对CP的新机械化，捕获了这些特性。开发Mech有两个核心技术挑战。首先，文献中的语义草图未正确捕获非确定性选择与并发的交互，因此我们制定了新语义。其次，在证明中管理所有这些特性很复杂，我们通过揭示编排、其语义中使用的运算符、EPP及其组合的新代数定律来解决。利用我们的开发，我们证明了EPP的完整性和正确性，并推导了投影网络的通信安全性和无死锁性，产生了迄今为止最广泛的CP机械化理论。
英文摘要：
Choreographic programming (CP) is a programming paradigm for the correct-by-construction development of concurrent and distributed systems: programmers write the intended overall behaviour of a system from a global perspective in a choreography, which is then automatically compiled into communicating endpoint programs by a procedure known as endpoint projection (EPP). The central promise is that the projected endpoint programs, when executed together, are behaviourally equivalent to the source choreography. Fulfilling this promise becomes delicate for expressive CP languages. Existing mechanisations of CP treat only restricted fragments, while textbook and general purpose language implementations with rich features leave crucial interactions informal. In particular, general branching in knowledge of choice, general recursion, and nondeterministic choice in choreographies have not yet been integrated in a machine-checked theory. We present Mech, a new mechanisation of CP in Lean 4 that captures these features. There are two central technical challenges in our development of Mech. First, the sketched semantics from the literature does not correctly capture how nondeterministic choice interacts with concurrency. We therefore formulate new semantics that align nondeterministic choreographic executions with the behaviours of projected endpoint programs. Second, managing all these features in proofs is complex. We address this by uncovering new algebraic laws for choreographies, the operators used in their semantics, EPP, and their combinations. Using our development, we prove completeness and soundness of EPP and derive communication safety and deadlock-freedom for projected networks, yielding the most extensive mechanised theory of CP to date.
