Session Types Go Dynamic or How to Verify Your Python Conversations

Rumyana Neykova
(Imperial College)

This paper presents the first implementation of session types in a dynamically-typed language - Python. Communication safety of the whole system is guaranteed at runtime by monitors that check the execution traces comply with an associated protocol. Protocols are written in Scribble, a choreography description language based on multiparty session types, with addition of logic formulas for more precise behaviour properties. The presented framework overcomes the limitations of previous works on the session types where all endpoints should be statically typed so that they do not permit interoperability with untyped participants. The advantages, expressiveness and performance of dynamic protocol checking are demonstrated through use case and benchmarks.

In Nobuko Yoshida and Wim Vanderbauwhede: Proceedings 5th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES 2013), Rome, Italy, 23rd March 2013, Electronic Proceedings in Theoretical Computer Science 137, pp. 95–102.
Published: 8th December 2013.

ArXived at: http://dx.doi.org/10.4204/EPTCS.137.8 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org