Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Sun 13 Jan 2019 14:20 - 15:10 at Sala VII - Session 3 Chair(s): Paola Giannini

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 this talk, 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 based on a formulation of asynchronous MPST enriched with interaction refinements: a collection of features related to the refinement of protocols, such as message-type refinements (value constraints) and value dependent control flow. 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. 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. 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.

Slides (BEAT2019_RUMI_Part1.pdf)9.50MiB
Slides (Part2) (BEAT2019_RUMI_Part2.pdf)9.20MiB

Rumyana Neykova is a lecturer at Brunel University London, previously completed a PhD degree under the supervision of Prof. Nobuko Yoshida at Imperial College London, where she was also research fellow. Her research interests are in the area of distributed systems and networks, as well as type systems and language design. Her PhD focuses on development and applications of a type theory (called session types) for runtime verification of concurrent and distributed systems.

Sun 13 Jan

beat-2019-papers
13:30 - 15:30: BEAT 2019 - Session 3 at Sala VII
Chair(s): Paola GianniniUniversita' del Piemonte Orientale
beat-2019-papers13:30 - 14:20
Talk
Jan HoffmannCarnegie Mellon University
beat-2019-papers14:20 - 15:10
Talk
Rumyana NeykovaBrunel University London
File Attached
beat-2019-papers15:10 - 15:30
Talk
Hans HüttelDepartment of Computer Science, Aalborg University, Antonio RavaraDepartment of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon and NOVA LINCS, Adrian FrancalanzaUniversity of Malta, Mario BravettiUniversità di Bologna
File Attached

Rumyana Neykova is a lecturer at Brunel University London, previously completed a PhD degree under the supervision of Prof. Nobuko Yoshida at Imperial College London, where she was also research fellow. Her research interests are in the area of distributed systems and networks, as well as type systems and language design. Her PhD focuses on development and applications of a type theory (called session types) for runtime verification of concurrent and distributed systems.