Session types are a formalism to codify the structure of a communication, using types to specify the communication protocol used. This formalism provides the coder a type-safe way of writing communication code according to a specific protocol.
In this talk, we will focus on the case of Multiparty session types (MSPT) and their application on F#. By supporting them, we help F# guarantee safe communication, e.g no deadlocks and communication mismatches.
We show a new application of generative type providers as to generate communication primitives automatically derived from a program specification. The result is a type-safe communication library for .Net where method signatures and the order of invocation dictated by a predefined communication protocol are statically checked. As a specification language for defining protocols, we use the Scribble languages, developed by the Mobility Research Group at Imperial College London.
Fahd is a Master student at Imperial College London, who has done his Master thesis on session types and their application over F#. New to the F# community and the language, he loves to speak and learn about it every day. Other than that, he loves spending his spare time learning about different theories and technologies, especially type theory and functional programming.