An implicitly-typed deadlock-free process calculus. (English) Zbl 0999.68532

Kobayashi, Naoki; Saito, Shin; Sumii, Eijiro

Palamidessi, Catuscia (ed.), CONCUR 2000 - Concurrency theory. 11th international conference, University Park, PA, USA, August 22-25, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1877, 489-503 (2000).

Summary: We extend Kobayashi and Sumii’s type system for the dead-lock-free \(\pi\)-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.
For the entire collection see [Zbl 0944.00069].

MSC:

68Q85

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)