Abstract: Session types is a typing discipline for concurrent and distributed processes that allows errors such as communication mismatches and deadlocks to be detected statically. Refinement types are types elaborated by logical constraints that allow richer and finer-grained specification of application properties, combining types with logical formulae that may refer to program values and can constrain types using arbitrary predicates. Type providers, developed in F#, are compile-time components for on-demand code generation. Their architecture relies on an open-compiler, where provider-authors implement a small interface that allows them to inject new names/types into the programming context as the program is written.
In these lecture series, I will present a library that integrates aspects from the above fields to realise practical applications of multiparty refinement session types (MPST) for any .Net language. Our library supports the specification and validation of distributed message passing protocols enriched with message-type refinements (value constraints) and value dependent control flow. The protocols are written in Scribble (a toolchain for MPST).
The combination of these aspects—session types for structured interactions, constraint solving from refinement types, and protocol-specific code generation enables the specification and implementation of enriched protocols in native F# (and any .Net-compiled language) without requiring language extensions or external pre-processing of user programs. The API generation happens on demand (while the developer is writing the program) and at compile-time (the generated API calls are directly integrated into the compiled binaries of the program).
We will discuss the formal foundations of the library, validation of Scribble protocols, the technical challenges of compile-time generation, and finally, we will practice type-driven development of several small- and large-scale protocols. We will conclude with a brief overview of other tools and techniques for API generation of Scribble protocols.

Slides: [X]
Practical Exercises: [X], [X]
The content in these slides was presented during the BehAPI 2019 Summer School in Leicester.