An implicitly-typed deadlock-free process calculus

Naoki Kobayashi, Shin Saito, Eijiro Sumii

Research output: Chapter in Book/Report/Conference proceedingConference contribution

37 Citations (Scopus)


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
Number of pages16
ISBN (Print)3540678972, 9783540678977
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


Other11th International Conference on Concurrency Theory, CONCUR 2000
Country/TerritoryUnited States
CityUniversity Park, PA

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


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

Cite this