SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Sun 15 Nov 2020 08:20 - 09:00 at SPLASH-VII - Posters Session 1
Sun 15 Nov 2020 20:20 - 21:00 at SPLASH-VII - Posters Session 1 Mirror

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

08:20 - 09:00
Posters Session 1Posters at SPLASH-VII +12h
08:20
40m
Poster
Formulog: Datalog for SMT-based Static AnalysisOOPSLA
Posters
Aaron Bembenek Harvard University, Michael Greenberg Pomona College, Stephen Chong Harvard University
08:20
40m
Poster
Analogy-Making as a Core Primitive in the Software Engineering ToolboxOnward! Papers
Posters
Matthew Sotoudeh University of California, Davis, Aditya V. Thakur University of California, Davis
08:20
40m
Poster
Row and Bounded Polymorphism via Disjoint PolymorphismECOOP
Posters
Ningning Xie The University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong, Xuan Bi The University of Hong Kong, Tom Schrijvers KU Leuven
08:20
40m
Poster
Gradual Verification of Recursive Heap Data StructuresOOPSLA
Posters
Jenna Wise Carnegie Mellon University, Johannes Bader Jane Street, Cameron Wong Jane Street, Jonathan Aldrich Carnegie Mellon University, Éric Tanter University of Chile, Joshua Sunshine Carnegie Mellon University
08:20
40m
Poster
Knowing When to Ask: Sound Scheduling of Name Resolution in Type Checkers Derived from Declarative SpecificationsOOPSLA
Posters
Arjen Rouvoet Delft University of Technology, Hendrik van Antwerpen Delft University of Technology, Casper Bach Poulsen Delft University of Technology, Robbert Krebbers Radboud University Nijmegen, Eelco Visser Delft University of Technology
08:20
40m
Poster
Owicki-Gries Reasoning for C11 RARECOOP
Posters
Sadegh Dalvandi University of Surrey, Simon Doherty University of Sheffield, Brijesh Dongol University of Surrey, Heike Wehrheim Paderborn University
08:20
40m
Poster
Demystifying DependenceOnward! Papers
Posters
08:20
40m
Poster
Can Advanced Type Systems Be Usable? An Empirical Study of Ownership, Assets, and Typestate in ObsidianOOPSLA
Posters
Michael Coblenz University of Maryland at College Park, Jonathan Aldrich Carnegie Mellon University, Brad A. Myers Carnegie Mellon University, Joshua Sunshine Carnegie Mellon University
08:20
40m
Poster
Multiparty Session Programming with Global Protocol CombinatorsECOOP
Posters
Keigo Imai Gifu University, Rumyana Neykova Brunel University London, Nobuko Yoshida Imperial College London, Shoji Yuen Nagoya University
08:20
40m
Poster
Static Race Detection and Mutex Safety and Liveness for Go ProgramsECOOP
Posters
Julia Gabet Imperial College London, Nobuko Yoshida Imperial College London
08:20
40m
Poster
CAMP: Cost-Aware Multiparty Session ProtocolsOOPSLA
Posters
David Castro-Perez Imperial College London, Nobuko Yoshida Imperial College London
08:20
40m
Poster
A Case Study in Language-Based Security: Building an I/O Library for WyvernOnward! Papers
Posters
Jennifer Fish Carnegie Mellon University, Darya Melicher Google, Jonathan Aldrich Carnegie Mellon University
08:20
40m
Poster
On the Unusual Effectiveness of Type-aware Operator Mutations for Testing SMT SolversOOPSLA
Posters
Dominik Winterer ETH Zurich, Chengyu Zhang East China Normal University, Zhendong Su ETH Zurich
08:20
40m
Poster
Reshape Your Layouts, Not Your Programs: A Safe Language Extension for Better Cache LocalityECOOP
Posters
Alexandros Tasos Imperial College London, Juliana Franco , Sophia Drossopoulou Imperial College London, Tobias Wrigstad Uppsala University, Sweden, Susan Eisenbach Imperial College London
08:20
40m
Poster
A Type-Directed Operational Semantics for a Calculus with a Merge OperatorECOOP
Posters
Xuejing Huang The University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
08:20
40m
Poster
Geometry Types for Graphics ProgrammingOOPSLA
Posters
Dietrich Geisler Cornell University, Irene Yoon University of Pennsylvania, Aditi Kabra Carnegie Mellon University, Horace He Cornell University, Yinnon Sanders Cornell University, Adrian Sampson Cornell University
20:20 - 21:00
Posters Session 1 MirrorPosters at SPLASH-VII
20:20
40m
Poster
Analogy-Making as a Core Primitive in the Software Engineering ToolboxOnward! Papers
Posters
Matthew Sotoudeh University of California, Davis, Aditya V. Thakur University of California, Davis
20:20
40m
Poster
Static Race Detection and Mutex Safety and Liveness for Go ProgramsECOOP
Posters
Julia Gabet Imperial College London, Nobuko Yoshida Imperial College London
20:20
40m
Poster
On the Unusual Effectiveness of Type-aware Operator Mutations for Testing SMT SolversOOPSLA
Posters
Dominik Winterer ETH Zurich, Chengyu Zhang East China Normal University, Zhendong Su ETH Zurich
20:20
40m
Poster
A Type-Directed Operational Semantics for a Calculus with a Merge OperatorECOOP
Posters
Xuejing Huang The University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
20:20
40m
Poster
Knowing When to Ask: Sound Scheduling of Name Resolution in Type Checkers Derived from Declarative SpecificationsOOPSLA
Posters
Arjen Rouvoet Delft University of Technology, Hendrik van Antwerpen Delft University of Technology, Casper Bach Poulsen Delft University of Technology, Robbert Krebbers Radboud University Nijmegen, Eelco Visser Delft University of Technology
20:20
40m
Poster
A Case Study in Language-Based Security: Building an I/O Library for WyvernOnward! Papers
Posters
Jennifer Fish Carnegie Mellon University, Darya Melicher Google, Jonathan Aldrich Carnegie Mellon University
20:20
40m
Poster
CAMP: Cost-Aware Multiparty Session ProtocolsOOPSLA
Posters
David Castro-Perez Imperial College London, Nobuko Yoshida Imperial College London
20:20
40m
Poster
Owicki-Gries Reasoning for C11 RARECOOP
Posters
Sadegh Dalvandi University of Surrey, Simon Doherty University of Sheffield, Brijesh Dongol University of Surrey, Heike Wehrheim Paderborn University
20:20
40m
Poster
Formulog: Datalog for SMT-based Static AnalysisOOPSLA
Posters
Aaron Bembenek Harvard University, Michael Greenberg Pomona College, Stephen Chong Harvard University
20:20
40m
Poster
Demystifying DependenceOnward! Papers
Posters
20:20
40m
Poster
Row and Bounded Polymorphism via Disjoint PolymorphismECOOP
Posters
Ningning Xie The University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong, Xuan Bi The University of Hong Kong, Tom Schrijvers KU Leuven
20:20
40m
Poster
Reshape Your Layouts, Not Your Programs: A Safe Language Extension for Better Cache LocalityECOOP
Posters
Alexandros Tasos Imperial College London, Juliana Franco , Sophia Drossopoulou Imperial College London, Tobias Wrigstad Uppsala University, Sweden, Susan Eisenbach Imperial College London
20:20
40m
Poster
Gradual Verification of Recursive Heap Data StructuresOOPSLA
Posters
Jenna Wise Carnegie Mellon University, Johannes Bader Jane Street, Cameron Wong Jane Street, Jonathan Aldrich Carnegie Mellon University, Éric Tanter University of Chile, Joshua Sunshine Carnegie Mellon University
20:20
40m
Poster
Multiparty Session Programming with Global Protocol CombinatorsECOOP
Posters
Keigo Imai Gifu University, Rumyana Neykova Brunel University London, Nobuko Yoshida Imperial College London, Shoji Yuen Nagoya University
20:20
40m
Poster
Can Advanced Type Systems Be Usable? An Empirical Study of Ownership, Assets, and Typestate in ObsidianOOPSLA
Posters
Michael Coblenz University of Maryland at College Park, Jonathan Aldrich Carnegie Mellon University, Brad A. Myers Carnegie Mellon University, Joshua Sunshine Carnegie Mellon University
20:20
40m
Poster
Geometry Types for Graphics ProgrammingOOPSLA
Posters
Dietrich Geisler Cornell University, Irene Yoon University of Pennsylvania, Aditi Kabra Carnegie Mellon University, Horace He Cornell University, Yinnon Sanders Cornell University, Adrian Sampson Cornell University