Programming communicating processes is challenging, because it requires writing separate programs that perform compatible send and receive actions at the right time during execution. Leaving this task to the programmer can easily lead to bugs. Choreographic programming addresses this challenge by equipping developers with high-level abstractions for codifying the desired communication structures from a global viewpoint. Given a choreography, implementations of the involved processes can be automatically generated by endpoint projection (EPP). While choreographic programming prevents manual mistakes in the implementation of communications, the correctness of a choreographic programming framework crucially hinges on the correctness of its complex compiler, which has motivated formalisation of theories of choreographic programming in theorem provers. In this paper, we build upon one of these formalisations to construct a toolchain that produces executable code from a choreography.

翻译：对通信进程进行编程极具挑战性，因为这要求编写独立的程序，使其在执行过程中恰当时刻执行兼容的发送与接收操作。若将此任务交由程序员处理，极易引发错误。编排式编程通过为开发者提供从全局视角规范所需通信结构的高级抽象来应对这一挑战。给定一个编排，可通过端点投影自动生成所涉及进程的实现代码。虽然编排式编程能防止通信实现中的人工错误，但编排式编程框架的正确性关键取决于其复杂编译器的正确性——这促使人们使用定理证明器对编排式编程理论进行形式化。本文基于其中一种形式化方法，构建了从编排生成可执行代码的工具链。