TY - JOUR
T1 - Parameterized, concurrent session types for asynchronous multi-actor interactions
AU - Charalambides, Minas
AU - Dinges, Peter
AU - Agha, Gul
N1 - Funding Information:
The authors would like to thank Karl Palmskog for his helpful comments. We would also like to thank the anonymous reviewers for their many suggestions, which have undoubtedly led to the maturement of this paper. This publication was made possible in part by a joint sponsorship from the Air Force Research Laboratory and the Air Force Office of Scientific Research under agreement number FA8750-11-2-0084 , and also a sponsorship from the National Science Foundation under grant number CCF-1438982 . The U.S. Government is authorized to reproduce and distribute reprints for Governmental purposes notwithstanding any copyright notation thereon.
Publisher Copyright:
© 2015 Elsevier B.V. All rights reserved.
PY - 2016/1/1
Y1 - 2016/1/1
N2 - Session types have been proposed as a means of statically verifying implementations of communication protocols. Although prior work has been successful for some classes of protocols, it does not cope well with parameterized, multi-actor scenarios with inherent asynchrony. For example, the sliding window protocol is not expressible in previously proposed session type notations. This article defines System-A: A novel session type system, as well the associated programming language that together overcome many of the limitations of prior work. With explicit support for asynchrony and concurrency, as well as multiple forms of parameterization, we demonstrate that System-A can be used for the static verification of a large class of asynchronous communication protocols.
AB - Session types have been proposed as a means of statically verifying implementations of communication protocols. Although prior work has been successful for some classes of protocols, it does not cope well with parameterized, multi-actor scenarios with inherent asynchrony. For example, the sliding window protocol is not expressible in previously proposed session type notations. This article defines System-A: A novel session type system, as well the associated programming language that together overcome many of the limitations of prior work. With explicit support for asynchrony and concurrency, as well as multiple forms of parameterization, we demonstrate that System-A can be used for the static verification of a large class of asynchronous communication protocols.
KW - Actors
KW - Concurrency
KW - Parameterized
KW - Session types
KW - Static
UR - http://www.scopus.com/inward/record.url?scp=84958999027&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84958999027&partnerID=8YFLogxK
U2 - 10.1016/j.scico.2015.10.006
DO - 10.1016/j.scico.2015.10.006
M3 - Article
AN - SCOPUS:84958999027
VL - 115-116
SP - 100
EP - 126
JO - Science of Computer Programming
JF - Science of Computer Programming
SN - 0167-6423
ER -