SPLASH 2023
Sun 22 - Fri 27 October 2023 Cascais, Portugal
Mon 23 Oct 2023 09:30 - 10:00 at Oceanus - Session 5 Chair(s): Ugo de'Liguoro

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 Oct

Displayed time zone: Lisbon change

09:00 - 10:30
Session 5PPDP at Oceanus
Chair(s): Ugo de'Liguoro Università di Torino
09:00
30m
Paper
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
30m
Paper
Termination in Concurrency, Revisited
PPDP
Joseph Paulus , Daniele Nantes-Sobrinho Imperial College London, Jorge A. Pérez University of Groningen
10:00
30m
Paper
Polymorphic Typestate for Session Types
PPDP
Hannes Saffrich University of Freiburg, Peter Thiemann University of Freiburg, Germany