Abstract

We extend Kobayashi and Sumii's type system for the deadlock-free Pi-calculus and develop a type reconstruction algorithm. Kobayashi and Sumii's type system is a generalization of Kobayashi, Pierce, and Turner's linear pi-calculus, and it helps high-level reasoning about concurrent programs by guaranteeing that communication on certain channels will eventually succeed. It can ensure, for example, that a process implementing a function really behaves like a function. However, because it lacked a type reconstruction algorithm and required rather complicated type annotations, it was impractical to apply it to real concurrent languages. We have therefore developed a type reconstruction algorithm for an extension of the type system. The key novelties that made it possible are generalization of the channel usage calculus (which was first introduced in Sumii and Kobayashi's previous type system) and a subusage relation.