TY - GEN
T1 - An implicitly-typed deadlock-free process calculus
AU - Kobayashi, Naoki
AU - Saito, Shin
AU - Sumii, Eijiro
PY - 2000
Y1 - 2000
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84885206872&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84885206872&partnerID=8YFLogxK
U2 - 10.1007/3-540-44618-4_35
DO - 10.1007/3-540-44618-4_35
M3 - Conference contribution
AN - SCOPUS:84885206872
SN - 3540678972
SN - 9783540678977
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 489
EP - 504
BT - CONCUR 2000 - Concurrency Theory
A2 - Palamidessi, Catuscia
PB - Springer Verlag
T2 - 11th International Conference on Concurrency Theory, CONCUR 2000
Y2 - 22 August 2000 through 25 August 2000
ER -