Termination (also known as \emph{strong normalization}) is a fundamental property in sequential programming models. A process is terminating if all its reduction sequences are of finite length. Termination is also important in concurrency in general, and in message-passing programs in particular. Indeed, a variety of type systems that enforce termination by typing have been developed in the last 20 years. Unfortunately, the precise relation between those type systems remains scarcely understood. In this paper, we rigorously compare different type systems for mobile processes from the unifying perspective of termination. Considering session types as a basic reference, we consider two different type systems that ensure termination: one follows Deng and Sangiorgi’s weight-based type system; the other is induced by Caires and Pfenning’s Curry-Howard correspondence between linear logic and session types. Our results precisely connect these very different systems and approaches, and shed light on the nature of (well-behaved) servers and client abstractions in concurrency.
Mon 23 OctDisplayed time zone: Lisbon change
09:00 - 10:30 | |||
09:00 30mPaper | Multicompatibility for Multiparty-Session Composition PPDP Franco Barbanera , Mariangiola Dezani Università di Torino, Lorenzo Gheri University of Liverpool, Nobuko Yoshida University of Oxford | ||
09:30 30mPaper | Termination in Concurrency, Revisited PPDP Joseph Paulus , Daniele Nantes-Sobrinho Imperial College London, Jorge A. Pérez University of Groningen | ||
10:00 30mPaper | Polymorphic Typestate for Session Types PPDP |