An Implicitly-Typed Deadlock-Free Process Calculus

Abstract. We extend Kobayashi and Sumii’s type system for the deadlock-free π-calculus and develop a type reconstruction algorithm. Kobayashi and Sumii’s type system 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, applying it to real concurrent languages was impractical. 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 usages (which specifies how each communication channel is used) and a subusage relation.

• Type: Conference
• Year: 2000
• Where: CONCUR
• Authors: Naoki Kobayashi, Shin Saito, Eijiro Sumii
• Keywords: CONCUR 2000, Distributed And Parallel Computing, Type Annotations, Type Reconstruction Algorithm, Type System