具有hacc的编译验证舞台设计
摘要：编程通信进程是具有挑战性的，因为它需要编写单独的程序，在执行过程中以正确的时间执行兼容的发送和接收操作。将这个任务留给程序员很容易导致错误。编舞式编程通过为开发人员提供高级抽象，从全局视角编码所需的通信结构，从而解决了这个挑战。给定一个舞蹈编程，可以通过端点投影（EPP）自动生成相关进程的实现。 虽然编舞式编程可以避免在通信实现中出现手动错误，但编舞式编程框架的正确性极大程度上取决于其复杂编译器的正确性，这就促使在定理证明器中形式化编舞式编程理论。在本文中，我们在其中一个形式化的基础上构建了一个工具链，该工具链从舞蹈编程中生成可执行代码。
作者：Lu''is Cruz-Filipe, Lovro Lugovi''c, Fabrizio Montesi
论文ID：2303.03972
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-03-08