An implicitly-typed deadlock-free process calculus

Naoki Kobayashi, Shin Saito, Eijiro Sumii

Research output: Chapter in Book/Report/Conference proceedingConference 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 languageEnglish
Title of host publicationCONCUR 2000 - Concurrency Theory
Subtitle of host publication11th International Conference, Proceedings
EditorsCatuscia Palamidessi
PublisherSpringer Verlag
Pages489-504
Number of pages16
ISBN (Print)3540678972, 9783540678977
DOIs
Publication statusPublished - 2000
Externally publishedYes
Event11th International Conference on Concurrency Theory, CONCUR 2000 - University Park, PA, United States
Duration: 2000 Aug 222000 Aug 25

Publication series

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

Other

Other11th International Conference on Concurrency Theory, CONCUR 2000
CountryUnited States
CityUniversity Park, PA
Period00/8/2200/8/25

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

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