University of Hertfordshire

A session type provider: Compile-time API generation of distributed protocols with refinements in F#

Research output: Contribution to conferencePaperpeer-review

  • Rumyana Neykova
  • Raymond Hu
  • Nobuko Yoshida
  • Fahd Abdeljallal
View graph of relations
Original languageEnglish
Number of pages10
Publication statusPublished - 24 Feb 2018
EventProceedings of the 27th International Conference on Compiler Construction - Vienan, Austria
Duration: 24 Feb 201825 Feb 2018


ConferenceProceedings of the 27th International Conference on Compiler Construction


We present a library for the specification and implementation of distributed protocols in native F# (and other .NET languages) based on multiparty session types (MPST). There are two main contributions. Our library is the first practical development of MPST to support what we refer to as interaction refinements: a collection of features related to the refinement of protocols, such as message-type refinements (value constraints) and message value dependent control flow. A well-typed endpoint program using our library is guaranteed to perform only compliant session I/O actions w.r.t. to the refined protocol, up to premature termination.

Second, our library is developed as a session type provider, that performs on-demand compile-time protocol validation and generation of protocol-specific .NET types for users writing the distributed endpoint programs. It is implemented by extending and integrating Scribble (a toolchain for MPST) with an SMT solver into the type providers framework. The safety guarantees are achieved by a combination of static type checking of the generated types for messages and I/O operations, correctness by construction from code generation, and automated inlining of assertions.


© 2018 Copyright held by the owner/author(s).

ID: 17769638