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 AprDisplayed 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:0030mTalk Asynchronous timed session types: duality and time-sensitive processesESOPLaura Bocchi University of Kent, Maurizio Murgia , Vasco T. Vasconcelos University of Lisbon, Portugal, Nobuko Yoshida Imperial College London Link to publication 14:3030mTalk Manifest Deadlock-Freedom for Shared Session TypesESOPStephanie Balzer Carnegie Mellon University, Bernardo Toninho Imperial College London, Frank Pfenning Carnegie Mellon University, USA Link to publication 15:0030mTalk A Categorical Model of an i/o-typed pi-calculusESOPKen Sakayori The University of Tokyo, Takeshi Tsukada University of Tokyo, Japan Link to publication 15:3030mTalk A Process Algebra for Link Layer ProtocolsESOP Link to publication