Refining multiparty session types

Abstract

A distributed system consists of various components working in coordination, usually following a specified protocol. Multiparty session types (MPST) are a typing discipline for distributed programming with message passing concurrency. The typing discipline provides a way to describe communication protocols as global types governing the overall communication structure. From global types, local types are derived for describing the behaviour of an individual component. This top-down design methodology provides a way to specify and implement multiparty communication protocols correctly. Communication protocols often contain constraints on payload data. While the original MPST theory provides support for basic payload types and ensures the absence of payload type mismatches, there is no way to capture data constraints using basic types. To address this limitation, we propose to incorporate refinement types into multiparty session types. Refinement types provide a lightweight way to describe and verify properties on data, and integrating refinement types into MPST allows properties and constraints on data to be specified and verified. In this thesis, we introduce a theory of refined multiparty session types, and a toolchain, Session*, for implementing refined protocols. On the theory side, we show that our extended theory retains desirable properties of MPST while improving expressivity. On the practical side, we target the F* programming language, and demonstrate a code generation approach that guarantees safety by construction.