Reversibility in the higher-order π-calculus
Reversibility in the higher-order π-calculus
复制标题
DOI：
10.1016/j.tcs.2016.02.019
复制
发表时间：
2016-04-25
影响因子：
1.1
通讯作者：
Stefani, Jean-Bernard
中科院分区：
文献类型：
--
作者：
Lanese, Ivan;Mezzina, Claudio Antares;Stefani, Jean-Bernard
可逆计算的概念因其在不同领域的应用，特别是在可靠系统的编程抽象研究中的应用，正吸引着越来越多的关注。在本文中，我们通过定义一种称为rho pi的可逆高阶π演算，延续了达诺斯（Danos）和克里文（Krivine）对可逆CCS的研究。我们证明了我们演算中的可逆性是因果一致的，并且用于支持rho中可逆性的因果信息与博雷亚莱（Boreale）和桑焦尔吉（Sangiorgi）所开发的π演算的因果语义中所使用的信息是一致的。最后，我们表明可以将rho pi忠实地编码为高阶π的一个变体，这大大改进了我们在本文会议版本中所得到的结果。© 2016爱思唯尔有限公司。保留所有权利。
The notion of reversible computation is attracting increasing interest because of its applications in diverse fields, in particular the study of programming abstractions for reliable systems. In this paper, we continue the study undertaken by Danos and Krivine on reversible CCS by defining a reversible higher-order pi-calculus, called rho pi. We prove that reversibility in our calculus is causally consistent and that the causal information used to support reversibility in rhos is consistent with the one used in the causal semantics of the pi-calculus developed by Boreale and Sangiorgi. Finally, we show that one can faithfully encode rho pi into a variant of higher-order pi, substantially improving on the result we obtained in the conference version of this paper. (C) 2016 Elsevier B.V. All rights reserved.