LFCS seminar: Ornela Dardha: Session types revisited
Apr 04, 2017
from 04:00 PM to 05:00 PM
|Add event to calendar||
Session types are a formalism to model structured communication-based programming. A binary session type describes communication by specifying the type and direction of data exchanged between two parties. We show that session types are encodable in standard pi-calculus types, relying on linear and variant types. Besides providing an expressivity result, the encoding: (i) removes redundancies in the syntax of session types, and (ii) yields standard properties of session types as straightforward corollaries, exploiting the corresponding properties of standard typed pi-calculus. The robustness of the encoding is tested on a few extensions of session types, including subtyping, polymorphism, and higher-order communications. In this talk we present the encoding and some of its applications.