Parameterized, concurrent session types for asynchronous multi-actor interactions

Minas Charalambides, Peter Dinges, Gul Agha

Research output: Contribution to journalArticlepeer-review


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.

Original languageEnglish (US)
Pages (from-to)100-126
Number of pages27
JournalScience of Computer Programming
StatePublished - Jan 1 2016


  • Actors
  • Concurrency
  • Parameterized
  • Session types
  • Static

ASJC Scopus subject areas

  • Software


Dive into the research topics of 'Parameterized, concurrent session types for asynchronous multi-actor interactions'. Together they form a unique fingerprint.

Cite this