A generic type system for the Pi-calculus
A generic type system for the Pi-calculus
复制标题
DOI：
10.1016/s0304-3975(03)00325-6
复制
发表时间：
2004-01-23
影响因子：
1.1
通讯作者：
Kobayashi, N
中科院分区：
文献类型：
--
作者：
Igarashi, A;Kobayashi, N
我们为pi-演算提出了一个通用的、强大的类型系统框架，并证明了作为它的实例，我们可以得到各种类型系统作为它的实例，这些类型系统保证了死锁自由和种族自由等非平凡性质。一个关键思想是将类型和类型环境表示为抽象进程：我们可以通过检查进程的类型环境的相应属性来检查进程的各种属性。该框架澄清了当前复杂类型系统的本质，并允许分担大量工作，例如类型保存的证明，从而使开发新的类型系统变得容易。(C)2003爱思唯尔B.V.保留所有权利。
We propose a general, powerful framework of type systems for the pi-calculus, and show that we can obtain as its instances a variety of type systems guaranteeing non-trivial properties like deadlock-freedom and race-freedom. A key idea is to express types and type environments as abstract processes: We can check various properties of a process by checking the corresponding proper-ties of its type environment. The framework clarifies the essence of recent complex type systems, and it also enables sharing of a large amount of work such as a proof of type preservation, making it easy to develop new type systems. (C) 2003 Elsevier B.V. All rights reserved.