An implicitly-typed deadlock-free process calculus

Naoki Kobayashi; Shin Saito; Eijiro Sumii

doi:10.1007/3-540-44618-4_35

An implicitly-typed deadlock-free process calculus

Naoki Kobayashi, Shin Saito, Eijiro Sumii

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

34 Citations (Scopus)

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.

Original language	English
Title of host publication	CONCUR 2000 - Concurrency Theory
Subtitle of host publication	11th International Conference, Proceedings
Editors	Catuscia Palamidessi
Publisher	Springer Verlag
Pages	489-504
Number of pages	16
ISBN (Print)	3540678972, 9783540678977
DOIs	https://doi.org/10.1007/3-540-44618-4_35
Publication status	Published - 2000
Externally published	Yes
Event	11th International Conference on Concurrency Theory, CONCUR 2000 - University Park, PA, United States Duration: 2000 Aug 22 → 2000 Aug 25

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	1877 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	11th International Conference on Concurrency Theory, CONCUR 2000
Country	United States
City	University Park, PA
Period	00/8/22 → 00/8/25

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/3-540-44618-4_35

Fingerprint Dive into the research topics of 'An implicitly-typed deadlock-free process calculus'. Together they form a unique fingerprint.

Cite this

Kobayashi, N., Saito, S., & Sumii, E. (2000). An implicitly-typed deadlock-free process calculus. In C. Palamidessi (Ed.), CONCUR 2000 - Concurrency Theory: 11th International Conference, Proceedings (pp. 489-504). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1877 LNCS). Springer Verlag. https://doi.org/10.1007/3-540-44618-4_35

An implicitly-typed deadlock-free process calculus. / Kobayashi, Naoki; Saito, Shin; Sumii, Eijiro.

CONCUR 2000 - Concurrency Theory: 11th International Conference, Proceedings. ed. / Catuscia Palamidessi. Springer Verlag, 2000. p. 489-504 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1877 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Kobayashi, N, Saito, S & Sumii, E 2000, An implicitly-typed deadlock-free process calculus. in C Palamidessi (ed.), CONCUR 2000 - Concurrency Theory: 11th International Conference, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 1877 LNCS, Springer Verlag, pp. 489-504, 11th International Conference on Concurrency Theory, CONCUR 2000, University Park, PA, United States, 00/8/22. https://doi.org/10.1007/3-540-44618-4_35

Kobayashi N, Saito S, Sumii E. An implicitly-typed deadlock-free process calculus. In Palamidessi C, editor, CONCUR 2000 - Concurrency Theory: 11th International Conference, Proceedings. Springer Verlag. 2000. p. 489-504. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/3-540-44618-4_35

Kobayashi, Naoki ; Saito, Shin ; Sumii, Eijiro. / An implicitly-typed deadlock-free process calculus. CONCUR 2000 - Concurrency Theory: 11th International Conference, Proceedings. editor / Catuscia Palamidessi. Springer Verlag, 2000. pp. 489-504 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{0b58e3db9748492f827bd98862d3b499,

title = "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.",

author = "Naoki Kobayashi and Shin Saito and Eijiro Sumii",

year = "2000",

doi = "10.1007/3-540-44618-4_35",

language = "English",

isbn = "3540678972",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "489--504",

editor = "Catuscia Palamidessi",

booktitle = "CONCUR 2000 - Concurrency Theory",

note = "11th International Conference on Concurrency Theory, CONCUR 2000 ; Conference date: 22-08-2000 Through 25-08-2000",

}

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 -