Sciweavers

CONCUR
2000
Springer

An Implicitly-Typed Deadlock-Free Process Calculus

13 years 8 months ago
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.
Naoki Kobayashi, Shin Saito, Eijiro Sumii
Added 02 Aug 2010
Updated 02 Aug 2010
Type Conference
Year 2000
Where CONCUR
Authors Naoki Kobayashi, Shin Saito, Eijiro Sumii
Comments (0)