Session Types for Me and You and Everyone We Know! - Zeeshan Lakhani

Zeeshan Lakhani explains session types as a formalism to model distributed communicating processes and provide runtime safety.

Concurrent and distributed systems are unwieldy, and many of the patterns we program them with are informally characterized. How can we provide safety mechanisms at runtime and structure inter-process communication? One approach is session types, a formalism to model distributed communicating processes, describing protocols as type abstractions. This talk will cover the basics of what session types are and how they provide a safety net for asynchronous interaction across our increasingly complex platforms and networks. The flow of this talk will start with the motivation for the need to formalize communication patterns across actors/channels/processes. Then, I’ll define what session types are and briefly describe their ongoing history. Finally, I’ll describe a couple specific approaches, geared around functional dynamic languages as a form of runtime rejection, for which session types can be applied.