School of Computing

Sep 16
15:00 - 16:00
PLAS: Keigo Imai, Gifu University, Japan
PLAS Group Seminar
Global Protocol Combinators: static structural multiparty sessions over simply-typed channels

In this work, we present Global Protocol Combinators (GPC), a shallow embedding of multiparty session types (MPSTs) into a minimal functional programming language, OCaml^M, with support for channel-based concurrency, structural subtyping and equi-recursive types.  GPC has the following ingredients: (1) global combinators -- a set of statically typed primitives for writing global protocol; (2) translation from global combinators to channel vectors -- a structured sequence of simply-typed i/o channels; and (3) a local calculus for programming message-passing computation. We prove that our language for global combinators is type-safe.  We show a behaviour-preserving encoding of MPSTs to OCaml^M and establish an operational correspondence between well-formed multiparty global protocols and well-typed global combinators.

Our implementation in OCaml is the first fully-static MPST implementation with support for session delegation. It safely (without explicit casts) realises multiparty communication over simply-typed i/o channels, preserving the order of interactions. We demonstrate global combinators on a plethora of examples.  Our evaluation shows that global combinators are more efficient (in terms of runtime performance), lightweight (no external verification tools are necessary) and more expressive (supports full-merging) than existing implementations.

Location

SW101,
Cornwallis South West,
University of Kent,
Canterbury,
Kent,
CT2 7NF
United Kingdom
Map

Details

Contact: O.Chitil
E: oc@kent.ac.uk
School of Computing

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 14/08/2015