Termination in Concurrency, Revisited - PPDP23

Explore a rigorous comparison of different type systems for mobile processes from the perspective of termination in this conference talk. Delve into the fundamental property of termination in sequential and concurrent programming models, with a focus on message-passing programs. Examine two distinct type systems that ensure termination: one based on Deng and Sangiorgi's weight-based approach, and another derived from Caires and Pfenning's Curry-Howard correspondence between linear logic and session types. Gain insights into the precise connections between these diverse systems and approaches, and uncover the nature of well-behaved servers and client abstractions in concurrency. Learn how session types serve as a basic reference in this comparative analysis, shedding light on the importance of termination in concurrent programming paradigms.