Write a Blog >>
Fri 23 Jun 2017 11:45 - 12:10 at Auditorium, Vertex Building - Types and Effects Chair(s): Philipp Haller

Multiparty Session Types (MPST) is a typing discipline for message-passing distributed processes that can ensure properties such as absence of communication errors and deadlocks, and protocol conformance. Can MPST provide a theoretical foundation for concurrent and distributed programming in “mainstream” languages?

We address this problem by (1) developing the first encoding of a full-fledged multiparty session pi-calculus into standard linear pi-calculus, and (2) using the encoding as the foundation of a practical toolchain for safe multiparty programming in Scala.

Our encoding is type-preserving and operationally sound and complete. Importantly for distributed applications, it preserves the choreographic nature of MPST and illuminates that multiparty sessions (and their safety properties) can be precisely represented with a decomposition into binary linear channels. Previous works have only studied the relation between (limited) multiparty sessions and binary sessions by orchestration means.

We exploit these results to implement an automated generation of Scala APIs for multiparty sessions. These APIs act as a layer on top of existing libraries for binary communication channels: this allows distributed multiparty systems to be safely implemented over binary transports, as commonly found in practice. Our implementation is also the first to support distributed multiparty delegation: our encoding yields it for free, via existing mechanisms for binary delegation.

Fri 23 Jun

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:10
Types and EffectsECOOP Research Papers at Auditorium, Vertex Building
Chair(s): Philipp Haller KTH Royal Institute of Technology
10:30
25m
Talk
Relaxed Linear References for Lock-free Programming
ECOOP Research Papers
Elias Castegren Uppsala University, Tobias Wrigstad Uppsala University
Link to publication Media Attached
10:55
25m
Talk
A Generic Approach to Flow-Sensitive Polymorphic Effects
ECOOP Research Papers
Colin Gordon Drexel University
Link to publication Pre-print Media Attached
11:20
25m
Talk
A Co-contextual Type Checker for Featherweight Java
ECOOP Research Papers
Edlira Kuci TU Darmstadt, Germany, Sebastian Erdweg TU Delft, Oliver Bračevac TU Darmstadt, Andi Bejleri TU Darmstadt, Germany, Mira Mezini TU Darmstadt
Link to publication Media Attached
11:45
25m
Talk
A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming
ECOOP Research Papers
Alceste Scalas Imperial College London, Ornela Dardha University of Glasgow, Raymond Hu Imperial College London, Nobuko Yoshida Imperial College London
Link to publication Media Attached