ECOOP 2020
Sun 15 - Tue 17 November 2020 Online Conference
co-located with SPLASH 2020
Sun 15 Nov 2020 17:40 - 18:00 at SPLASH-I - S-6 Chair(s): Shigeru Chiba, Tiark Rompf
Mon 16 Nov 2020 05:40 - 06:00 at SPLASH-I - S-6 Chair(s): Olivier Flückiger, Jeremy Gibbons

Multiparty Session Types (MPST) is a typing discipline for communication protocols. It ensures the absence of communication errors and deadlocks for well-typed communicating processes. The state of the art implementations of the MPST theory rely on (1) runtime linearity checks to ensure correct usage of communication channels and (2) external domain-specific languages for specifying and verifying of multiparty protocols.

To overcome these limitations, we propose a library for programming with global combinators – a set of functions for writing and verifying multiparty protocols in OCaml. Local behaviours for all processes in a protocol are inferred at once from a global combinator. We formalise global combinators and prove a sound realisability of global combinators – a well-typed global combinator derives a set of local types, by which typed endpoint programs can ensure type and communication safety. Our approach enables fully-static verification and implementation of the whole protocol, from the protocol specification to the process implementations, to happen in the same language.

We compare our implementation to untyped and continuation-passing style implementations, and demonstrate its expressiveness by implementing a plethora of protocols. We show our library can interoperate with existing libraries and services, implementing DNS (Domain Name Service) protocol and the OAuth (Open Authentication) protocol.

Sun 15 Nov

Displayed time zone: Central Time (US & Canada) change

17:00 - 18:20
S-6Research Papers at SPLASH-I +12h
Chair(s): Shigeru Chiba The University of Tokyo, Tiark Rompf Purdue University
17:00
20m
Talk
Static Race Detection and Mutex Safety and Liveness for Go Programs
Research Papers
Julia Gabet Imperial College London, Nobuko Yoshida Imperial College London
Link to publication DOI Media Attached
17:20
20m
Talk
Reference immutability for DOT
Research Papers
Vlastimil Dort Charles University, Ondřej Lhoták University of Waterloo
Link to publication DOI Media Attached
17:40
20m
Talk
Multiparty Session Programming with Global Protocol Combinators
Research Papers
Keigo Imai Gifu University, Rumyana Neykova Brunel University London, Nobuko Yoshida Imperial College London, Shoji Yuen Nagoya University
Link to publication DOI Media Attached
18:00
20m
Talk
Scala with Explicit Nulls
Research Papers
Abel Nieto Aarhus University, Yaoyu Zhao University of Waterloo, Ondřej Lhoták University of Waterloo, Angela Chang University of Waterloo, Justin Pu University of Waterloo
Link to publication DOI Pre-print Media Attached

Mon 16 Nov

Displayed time zone: Central Time (US & Canada) change

05:00 - 06:20
S-6Research Papers at SPLASH-I
Chair(s): Olivier Flückiger Northeastern University, Jeremy Gibbons Department of Computer Science, University of Oxford
05:00
20m
Talk
Static Race Detection and Mutex Safety and Liveness for Go Programs
Research Papers
Julia Gabet Imperial College London, Nobuko Yoshida Imperial College London
Link to publication DOI Media Attached
05:20
20m
Talk
Reference immutability for DOT
Research Papers
Vlastimil Dort Charles University, Ondřej Lhoták University of Waterloo
Link to publication DOI Media Attached
05:40
20m
Talk
Multiparty Session Programming with Global Protocol Combinators
Research Papers
Keigo Imai Gifu University, Rumyana Neykova Brunel University London, Nobuko Yoshida Imperial College London, Shoji Yuen Nagoya University
Link to publication DOI Media Attached
06:00
20m
Talk
Scala with Explicit Nulls
Research Papers
Abel Nieto Aarhus University, Yaoyu Zhao University of Waterloo, Ondřej Lhoták University of Waterloo, Angela Chang University of Waterloo, Justin Pu University of Waterloo
Link to publication DOI Pre-print Media Attached