Forum Numerica - On sessions, linear logic and unbounded interactions

Session types are descriptions of communication protocols as types. In a paper presented at CONCUR 2010, Luís Caires and Frank Pfenning have shown that there is a tight and natural correspondence between session types and linear logic propositions, and between session type systems and the proof rules of linear logic.  Since then, a large number of session type systems inspired by linear logic have been studied. Among the advantages of these type systems is the fact that they are able to enforce valuable properties such as the absence of deadlocks and livelocks without the burden of additional type structure.
In fact, these properties essentially come "for free" as the consequence of the cut elimination property of linear logic. A downside of these type systems is that some natural processes, in particular those involved in arbitrarily long interactions, are inherently ill typed since they would correspond to linear logic proofs admitting arbitrarily long cut reduction sequences.
In the first part of this seminar I will provide a gentle introduction to session typing based on linear logic.
In the second part, I will illustrate a conservative extension of linear logic that allows us to deal with (some) processes involved in arbitrarily long interactions while retaining all of the valuable properties inherited from the logical approach.

Luca Padovani is an associate professor in Computer Science at the Computer Science Division of the School of Science and Technology of the University of Camerino. His research interests span both theory and practice in the areas of programming languages, type systems, concurrency theory, distributed computing and formal verification.
https://boystrange.github.io