University of Hertfordshire

By the same authors

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

Conference

ConferenceProceedings of the 27th International Conference on Compiler Construction
CountryAustria
CityVienan
Period24/02/1825/02/18

Abstract

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.

Notes

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

ID: 17769638