Type reconstruction for linear pi-calculus with I/O subtyping
Atsushi Igarashi · 2000
Powerful concurrency primitives in recent concurrent languages and thread libraries provide great exibility about implementation of high-level features like concurrent objects. However, they are so low-level that they often make it dicult to check global correctness of programs or to perform non-trivial code optimization, such as elimination of redundant communication. In order to overcome those problems, advanced type systems for inputonly /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 recons...