2012/08/22 by Minas Charalambides, Peter Dinges, Gul Agha
Computer Science · #cs.PL #cs.DC
paper · pdf · doi:10.4204/eptcs.91.2
published as EPTCS 91, 2012, pp. 16-30 · In Proceedings FOCLASA 2012, arXiv:1208.4327
arxiv created 2012/08/22 · arxiv updated 2012/08/24
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.