A Higher-Order Distributed Calculus with Name Creation
A Higher-Order Distributed Calculus with Name Creation
复制标题
具有名称创建的高阶分布式微积分
DOI：
10.1109/lics.2012.63
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Eijiro Sumii
中科院分区：
文献类型：
--
作者：
Adrien Pierard;Eijiro Sumii
本文介绍了HOpiPn，具有钝化和名称创建的高阶pi演算，并发展了这种演算的等价理论。钝化[施密特和Stefani]是一种语言结构，它优雅地建模了高阶分布式行为，如故障，迁移或复制（例如，当正在运行的进程或虚拟机被复制时），并且名称创建包括生成一个新的名称而不是隐藏一个。结合高阶分布，名称创建导致与名称隐藏不同的语义，并且更接近分布式系统的实现。我们定义了这个新的微积分理论的声音和完整的环境互模拟证明减少封闭倒钩等价和（合理的形式）同余。我们还定义了环境模拟来证明行为近似，并使用这些理论来显示等价或近似的非平凡的例子。这些例子不能用以前的理论来证明，这些理论要么在过程重复和名称限制的情况下是不健全或不完整的，要么需要在一般背景下进行普适量化。
This paper introduces HOpiPn, the higher-order pi-calculus with passivation and name creation, and develops an equivalence theory for this calculus. Passivation [Schmitt and Stefani] is a language construct that elegantly models higher-order distributed behaviours like failure, migration, or duplication (e.g. when a running process or virtual machine is copied), and name creation consists in generating a fresh name instead of hiding one. Combined with higher-order distribution, name creation leads to different semantics from name hiding, and is closer to implementations of distributed systems. We define for this new calculus a theory of sound and complete environmental bisimulation to prove reduction-closed barbed equivalence and (a reasonable form of) congruence. We furthermore define environmental simulations to prove behavioural approximation, and use these theories to show non-trivial examples of equivalence or approximation. Those examples could not be proven with previous theories, which were either unsound or incomplete under the presence of process duplication and name restriction, or else required universal quantification over general contexts.