About Event

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: as far as types are concerned, any message can be received at any stage. That leads to code that has to handle a lot of illegal state, as we will demonstrate on an example.

In an attempt to make the illegal state unrepresentable, we will arrive at an encoding of session types. We will discover that session types 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, we will present Libretto, an experimental Scala library/DSL with an encoding of session types that checks linearity before program execution.