Parameterized Concurrent Multi-Party Session Types

Minas Charalambides
(University of Illinois at Urbana-Champaign)
Peter Dinges
(University of Illinois at Urbana-Champaign)
Gul Agha
(University of Illinois at Urbana-Champaign)

Session types have been proposed as a means of statically verifying implementations of communication protocols. Although prior work has been successful in verifying some classes of protocols, it does not cope well with parameterized, multi-actor scenarios with inherent asynchrony. For example, the sliding window protocol is inexpressible in previously proposed session type systems. This paper describes System-A, a new typing language which overcomes many of the expressiveness limitations of prior work. System-A explicitly supports asynchrony and parallelism, as well as multiple forms of parameterization. We define System-A and show how it can be used for the static verification of a large class of asynchronous communication protocols.

In Natallia Kokash and António Ravara: Proceedings 11th International Workshop on Foundations of Coordination Languages and Self Adaptation (FOCLASA 2012), Newcastle, U.K., September 8, 2012, Electronic Proceedings in Theoretical Computer Science 91, pp. 16–30.
Published: 15th August 2012.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: