Lightening Global Types

Tzu-chun Chen
(Dipartimento di Informatica, Universita' di Torino, Italy)

Global session types prevent participants from waiting for never coming messages. Some interactions take place just for the purpose of informing receivers that some message will never arrive or the session is terminated. By decomposing a big global type into several light global types, one can avoid such kind of redundant interactions. Lightening global types gives us cleaner global types, which keep all necessary communications. This work proposes a framework which allows to easily decompose global types into light global types, preserving the interaction sequences of the original ones but for redundant interactions.

In Alastair F. Donaldson and Vasco T. Vasconcelos: Proceedings 7th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES 2014), Grenoble, France, 12 April 2014, Electronic Proceedings in Theoretical Computer Science 155, pp. 38–46.
Published: 12th June 2014.

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