Mixed Choices: Taming Failures with Session Types in Erlang

What attendees will learn

Distributed systems are notoriously difficult to reason about. Timeouts, failures, and race conditions are often treated as edge cases hidden deep inside application logic. This workshop introduces multiparty session types, a formal approach to describing communication protocols between distributed processes, and shows how mixed choice extends these protocols to model real-world failure scenarios.

Participants will work with a toolchain that validates protocol specifications and generates Erlang gen_statem code, producing OTP-compliant state machines with safety guarantees built in. Through practical examples, attendees will learn how to make protocol structure explicit and avoid implementing delicate concurrency logic by hand.

Requirements

Basic familiarity with functional programming concepts is expected. Some exposure to concurrent or distributed systems is helpful but not required. No prior knowledge of session types or formal methods is necessary.

Attendees should bring a laptop with Docker installed and running.

Workshop plan

• Introduction to session types and distributed protocol design.
• Understanding mixed choice and modelling failures, timeouts, and race conditions.
• Reasoning about global protocols and their distributed realizations.
• Generating and inspecting Erlang gen_statem code.
• Implementing, compiling, and running a complete Erlang example.
• Wrap-up and Q&A.

Target audience

Functional programmers interested in distributed systems, concurrency, protocol design, or formal methods. It is particularly relevant for Erlang and Elixir practitioners, although the ideas apply across languages and platforms.