π-calculus, Session Types research at Imperial College
Our group’s Masters project student Fahd Adeljallal gave a talk titled Session Types with Fahd Abdeljallal in a recent F#unctional Londoners Meetup Group meeting on his Masters project which applied Multiparty Session Types on F#.
Abstract:
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 (MPST) 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 language, developed by the Mobility Research Group at Imperial College London.