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. © Springer-Verlag Berlin Heidelberg 2000.
CITATION STYLE
Kobayashi, N., Saito, S., & Sumii, E. (2000). An implicitly-typed deadlock-free process calculus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1877 LNCS, pp. 489–504). Springer Verlag. https://doi.org/10.1007/3-540-44618-4_35
Mendeley helps you to discover research relevant for your work.