Multiparty session type-safe web development with static linearity
Modern web applications can now offer desktop-like experiences from within the browser, thanks to technologies such as WebSockets, which enable low-latency duplex communication between the browser and the server. While these advances are great for the user experience, they represent a new responsibility for web developers who now need to manage and verify the correctness of the now more complex now and potentially stateful interactions in their application.
In this paper, we present a technique for developing interactive web applications that are statically guaranteed to communicate following a given protocol. First, the global interaction protocol is described in the Scribble protocol language – based on multiparty session types. Scribble protocols are checked for well-formedness, and then each role is projected to a Finite State Machine representing the structure of communication from the perspective of the role. We use source code generation and a novel type-level encoding of FSMs using multi-parameter type classes to leverage the type system of the target language to guarantee type-safe programs conform to the communication protocol.
Sun 7 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
13:30 - 15:30
IIIPLACES at S8
Chair(s): Vasco T. Vasconcelos University of Lisbon, Portugal
|Keynote: Shared Session Types for Safe, Practical Concurrency|
Stephanie Balzer Carnegie Mellon University
|Multiparty session type-safe web development with static linearity|
Jonathan King Habito and Imperial College London, Nicholas Ng Imperial College London, Nobuko Yoshida Imperial College London
|Service Equivalence via Multiparty Session Type Isomorphisms|
Assel Altayeva Imperial College London, Nobuko Yoshida Imperial College London