Session Types with Runtime Adaptation: Overview and Examples

Cinzia Di Giusto
Jorge A. Pérez

In recent work, we have developed a session types discipline for a calculus that features the usual constructs for session establishment and communication, but also two novel constructs that enable communicating processes to be stopped, duplicated, or discarded at runtime. The aim is to understand whether known techniques for the static analysis of structured communications scale up to the challenging context of context-aware, adaptable distributed systems, in which disciplined interaction and runtime adaptation are intertwined concerns. In this short note, we summarize the main features of our session-typed framework with runtime adaptation, and recall its basic correctness properties. We illustrate our framework by means of examples. In particular, we present a session representation of supervision trees, a mechanism for enforcing fault-tolerant applications in the Erlang language.

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. 21–32.
Published: 8th December 2013.

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