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

Rumyana Neykova, Raymond Hu, Nobuko Yoshida, Fahd Abdeljallal

    Research output: Contribution to conferencePaperpeer-review

    17 Citations (Scopus)

    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.
    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
    Country/TerritoryAustria
    CityVienan
    Period24/02/1825/02/18

    Fingerprint

    Dive into the research topics of 'A session type provider: Compile-time API generation of distributed protocols with refinements in F#'. Together they form a unique fingerprint.

    Cite this