Typed Interaction with Session Types

Tomas Mikula

Tomas Mikula
Senior Software Engineer at Barclays
About This 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.

Get your TypeVille Package now!
Immerse yourself into TypeSafety world

Experience something like never before - an all-inclusive tech conference in the Polish mountains