Actor 模型到 Haskell 的一种保持资源消耗的形式化翻译
编程语言
2016-08-11 v2 计算机科学中的逻辑
摘要
我们提出了一种从具有协作调度的基于 Actor 的语言到函数式语言 Haskell 的形式化翻译。该翻译的正确性依据源语言的形式语义和目标语言（即 Haskell 的一个子集）的高层操作语义得到了证明。主要正确性定理以 Actor 程序操作语义与其翻译之间的模拟关系来表述。这使得我们能够进一步证明资源消耗在此翻译过程中得以保持，因为我们建立了原始执行轨迹与 Haskell 翻译后执行轨迹的成本等价性。
引用
@article{arxiv.1608.02896,
title = {A Formal, Resource Consumption-Preserving Translation of Actors to Haskell},
author = {Elvira Albert and Nikolaos Bezirgiannis and Frank de Boer and Enrique Martin-Martin},
journal= {arXiv preprint arXiv:1608.02896},
year = {2016}
}
备注
Pre-proceedings paper presented at the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016), Edinburgh, Scotland UK, 6-8 September 2016 (arXiv:1608.02534)