Statically verified refinements for multiparty protocols

摘要: With distributed computing becoming ubiquitous in the modern era, safe 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 aspects, and employ simple system payloads, protocols real world usually contain constraints payload. We introduce refined (RMPST), extension of MPST, that express data dependent via refinement types. implementation RMPST, toolchain called Session*, using Scribble, protocols, targeting F*, verification-oriented functional language. Users can describe protocol Scribble implement endpoints F* refinement-typed APIs generated from protocol. The compiler then statically verify refinements. Moreover, we use novel approach callback-styled API generation, providing static linearity guarantees with inversion control. evaluate our examples show it has little overhead compared to naive implementation, while underlying theory.