Typechecking safe process synchronization

Eduardo Bonelli, Adriana Compagnoni, Elsa Gunter

Research output: Contribution to journalConference articlepeer-review

11 Scopus citations

Abstract

Session types describe the interactions between two parties within multi-party communications. They constitute a communication protocol in the sense that the order and type of interactions between two parties are specified. For their part, correspondence assertions provide a mechanism for synchronization. When session types and correspondence assertions are combined, they are able to describe synchronization across different communication sessions, yielding a rich language for imposing expressive interaction patterns in multi-party communications. This paper studies the typechecking problem for Iris, a typed π-calculus that combines session types and correspondence assertions. We define a typechecking algorithm and prove that it is sound and complete with respect to the typing rules. Furthermore, we show that the typing system satisfies the minimum effects property. Although session types have been extensively studied in the past few years, to our knowledge this is the first proof of decidability of typechecking for a type system with session types.

Original languageEnglish
Pages (from-to)3-22
Number of pages20
JournalElectronic Notes in Theoretical Computer Science
Volume138
Issue number1
DOIs
StatePublished - 9 Sep 2005
EventProceedings of the Workshop on the Foundations of Global Ubiquitous Computing (FGUC 2004) -
Duration: 3 Sep 20043 Sep 2004

Keywords

  • Concurrency
  • Type systems
  • Typechecking
  • π-calculus

Fingerprint

Dive into the research topics of 'Typechecking safe process synchronization'. Together they form a unique fingerprint.

Cite this