TY - JOUR
T1 - Typechecking safe process synchronization
AU - Bonelli, Eduardo
AU - Compagnoni, Adriana
AU - Gunter, Elsa
PY - 2005/9/9
Y1 - 2005/9/9
N2 - 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.
AB - 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.
KW - Concurrency
KW - Type systems
KW - Typechecking
KW - π-calculus
UR - http://www.scopus.com/inward/record.url?scp=24344483453&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=24344483453&partnerID=8YFLogxK
U2 - 10.1016/j.entcs.2005.05.002
DO - 10.1016/j.entcs.2005.05.002
M3 - Conference article
AN - SCOPUS:24344483453
SN - 1571-0661
VL - 138
SP - 3
EP - 22
JO - Electronic Notes in Theoretical Computer Science
JF - Electronic Notes in Theoretical Computer Science
IS - 1
T2 - Proceedings of the Workshop on the Foundations of Global Ubiquitous Computing (FGUC 2004)
Y2 - 3 September 2004 through 3 September 2004
ER -