Open Systems Laboratory at Illinois

Parameterized, concurrent session types for asynchronous multi-actor interactions

By Minas Charalambides, Peter Dinges, and Gul A. Agha. Science of Computer Programming, 115-116:100–126, 2016.

Publisher Link:


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. Session types offer static guarantees for concurrent code. Benefits of our system include:It can handle a parameterized number of actors (multi-actor programs).It can handle parameterized concurrency.It can handle asynchronous communication.It includes novel parameterized operators, such as one to express atomicity constraints.It deals with a series of cases that prior work could not handle.


    author = "Charalambides, Minas and Dinges, Peter and Agha, Gul
    title = "Parameterized, concurrent session types for asynchronous
             multi-actor interactions",
    biburl =
    doi = "10.1016/j.scico.2015.10.006",
    journal = "Science of Computer Programming",
    pages = "100--126",
    timestamp = "Wed, 14 Jun 2017 01:00:00 +0200",
    url = "",
    volume = "115-116",
    year = "2016",