Type reconstruction for linear π-calculus with I/O subtyping
Type reconstruction for linear π-calculus with I/O subtyping
复制标题
DOI：
10.1006/inco.2000.2872
复制
发表时间：
2000-08-25
影响因子：
1
通讯作者：
Kobayashi, N
中科院分区：
文献类型：
--
作者：
Igarashi, A;Kobayashi, N
最近的并发语言和线程库中强大的并发原始图为实施高级功能（如并发对象）提供了极大的灵活性。但是，它们是如此低级，以至于通常使检查程序的全局正确性或执行非平凡的代码优化，例如消除冗余通信。为了克服这些问题，最近已经研究了用于仅输入/仅输出/仅输出通道和线性（使用）通道的高级类型系统，但是这些类型系统的类型重建问题仍然开放，因此，它们的应用程序应用于并发编程语言受到限制。在本文中，我们开发了针对Kobayashi，Pierce和Turner的线性通道类型系统的类型重建算法，它具有Pierce和Sangiorgi的亚型，基于仅输入/仅输出的通道类型，并证明了算法的正确性。据我们所知，以前没有这些类型系统闻名的完整类型重建算法。我们已经实施了其中一种算法，并将其纳入了并发语言HACL的编译器中。本文还显示了有关该算法及其在编译时间优化的应用的一些实验结果。 （c）2000学术出版社。
Powerful concurrency primitives in recent concurrent languages and thread libraries provide great flexibility about implementation of high-level features like concurrent objects. However, they are so low-level that they often make it difficult to check global correctness of programs or to perform nontrivial code optimization, such as elimination of redundant communication. In order to overcome those problems, advanced type systems for input-only/output-only channels and linear (use-once) channels have been recently studied, but the type reconstruction problem for those type systems remained open, and therefore, their applications to concurrent programming languages have been limited. In this paper, we develop type reconstruction algorithms for variants of Kobayashi, Pierce, and Turner's linear channel type system with Pierce and Sangiorgi's subtyping based on input-only/output-only channel types and prove correctness of the algorithms. To our knowledge, no complete type reconstruction algorithm has been previously known for those type systems. We have implemented one of the algorithms and incorporated it into the compiler of the concurrent language HACL. This paper also shows some experimental results on the algorithm and its application to compile-time optimizations. (C) 2000 Academic Press.