Typed Interaction with Session Types
As interaction between two stateful components unfolds, the set of acceptable messages changes at each step. Session types change with the progressing interaction, thus providing type-safety at each step. Conventional approaches to typed interaction fail to keep track of the ever-changing state in types where any message can be received at any stage. That leads to code handling a lot of illegal state, as he will demonstrate with an example.
To make the illegal state unrepresentable, Tomas will arrive at an encoding of session types and discover that they require linearity, i.e., the property that each resource is consumed exactly once. However, linearity checking is not widely supported in mainstream programming languages. Finally, Tomas will present Libretto, an experimental Scala library/DSL with an encoding of session types that checks linearity before program execution.