ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Wed 10 Apr 2019 14:30 - 15:00 at SUN II - Concurrency and Distribution Chair(s): Luca Padovani

Shared session types generalize the Curry-Howard correspondence between intuitionistic linear logic and the session-typed $\pi$-calculus with adjoint modalities that mediate between linear and shared session types, giving rise to a programming model where shared channels must be used according to a lock discipline of acquire-release. While this generalization greatly increases the range of programs that can be written, the gain in expressiveness comes at the cost of deadlock-freedom, a property which holds for many linear session type systems. In this paper, we develop a type system for logically-shared sessions in which types capture not only the interactive behavior of processes but also constrain the order of resources (i.e., shared processes) they may acquire. This type-level information is then used to rule out cyclic dependencies among acquires and synchronization points, resulting in a system that ensures deadlock-free communication for well-typed processes in the presence of shared sessions, higher-order channel passing and recursive processes. We illustrate our approach on a series of examples, showing that it rules out deadlocks in circular networks of both shared and linear recursive processes, while still being permissive enough to type concurrent implementations of shared imperative data structures as processes.

Wed 10 Apr

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

14:00 - 16:00
Concurrency and DistributionESOP at SUN II
Chair(s): Luca Padovani University of Turin
14:00
30m
Talk
Asynchronous timed session types: duality and time-sensitive processes
ESOP
Laura Bocchi University of Kent, Maurizio Murgia , Vasco T. Vasconcelos University of Lisbon, Portugal, Nobuko Yoshida Imperial College London
Link to publication
14:30
30m
Talk
Manifest Deadlock-Freedom for Shared Session Types
ESOP
Stephanie Balzer Carnegie Mellon University, Bernardo Toninho Imperial College London, Frank Pfenning Carnegie Mellon University, USA
Link to publication
15:00
30m
Talk
A Categorical Model of an i/o-typed pi-calculus
ESOP
Ken Sakayori The University of Tokyo, Takeshi Tsukada University of Tokyo, Japan
Link to publication
15:30
30m
Talk
A Process Algebra for Link Layer Protocols
ESOP
Link to publication