With distributed computing becoming ubiquitous in the modern era, safe
distributed programming is an open challenge. To address this, multiparty
session types (MPST) provide a typing discipline for message-passing
concurrency, guaranteeing communication safety properties such as deadlock
freedom.
While originally MPST focus on the communication aspects, and employ a simple
typing system for communication payloads, communication protocols in the real
world usually contain constraints on the payload. We introduce refined
multiparty session types (RMPST), an extension of MPST, that express data
dependent protocols via refinement types on the data types.
We provide an implementation of RMPST, in a toolchain called Session*, using
Scribble, a multiparty protocol description toolchain, and targeting F*, a
verification-oriented functional programming language. Users can describe a
protocol in Scribble and implement the endpoints in F* using refinement-typed
APIs generated from the protocol. The F* compiler can then statically verify
the refinements. Moreover, we use a novel approach of callback-styled API
generation, providing static linearity guarantees with the inversion of
control. We evaluate our approach with real world examples and show that it has
little overhead compared to a na\"ive implementation, while guaranteeing safety
properties from the underlying theory.