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 -