认证编舞汇编
Certifying Choreography Compilation
摘要：
编排编程是开发并发和分布式系统的一种范式，其中程序是从全局角度定义通信进程应该执行的计算和交互的编排。编排编译将编排转换为流程行为的本地定义，作为流程演算中的术语给出。证明编排编译的正确性是具有挑战性和容易出错的，因为它需要在不同的范式（全局交互与本地操作）中关联语言，并处理证明案例的组合爆炸。我们提出了第一个认证程序的编排编译的非平凡的舞蹈语言支持递归。
英文摘要：
Choreographic programming is a paradigm for developing concurrent and distributed systems, where programs are choreographies that define, from a global viewpoint, the computations and interactions that communicating processes should enact. Choreography compilation translates choreographies into the local definitions of process behaviours, given as terms in a process calculus. Proving choreography compilation correct is challenging and error-prone, because it requires relating languages in different paradigms (global interactions vs local actions) and dealing with a combinatorial explosion of proof cases. We present the first certified program for choreography compilation for a nontrivial choreographic language supporting recursion.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
