使用 hacc 的编舞程序认证编译
编程语言
2023-03-08 v1
摘要
编写通信进程具有挑战性，因为这需要编写独立的程序，在执行期间的正确时刻执行兼容的发送和接收动作。将这一任务留给程序员很容易导致错误。编舞式编程（choreographic programming）通过为开发者提供高层抽象，从全局视角编纂所需的通信结构，以应对这一挑战。给定编舞（choreography），相关进程的实现的可以通过端点投影（EPP）自动生成。虽然编舞式编程防止了通信实现中的人工错误，但编舞式编程框架的正确性关键取决于其复杂编译器的正确性，这促使人们在定理证明器中形式化了编舞式编程理论。在本文中，我们基于其中一种形式化工作构建了一个工具链，该工具链可从编舞生成可执行代码。
引用
@article{arxiv.2303.03972,
title = {Certified Compilation of Choreographies with hacc},
author = {Luís Cruz-Filipe and Lovro Lugović and Fabrizio Montesi},
journal= {arXiv preprint arXiv:2303.03972},
year = {2023}
}