Bannière EUR DS4H - Digital Systems for Humans EUR DS4H - Digital Systems for Humans

 

Digital Systems for Humans (DS4H) est l'une des huit écoles universitaires de recherche thématiques d'Université Côte d'Azur. Elle s'intéresse aux aspects scientifiques, technologiques et humains de la digitalisation de la société. Sur le volet pédagogique, DS4H propose 5 masters "coeur" (majeures) en Informatique, Electronique, MIAGE, Droit du numérique et Stratégie digitale-Management du numérique et de l'innovation. Elle délivre des doctorats avec les écoles doctorales STIC,  DESPEG et SHAL. Sur le volet scientifique, DS4H mène un programme de recherche pluridisciplinaire impliquant 13 laboratoires dans les domaines du numérique et des sciences sociales.

Forum Numerica - Luca Padovani: "On sessions, linear logic and unbounded interactions"

12 janvier 2023
01:07:48
Nombre de vues 15
Nombre d’ajouts dans une liste de lecture 0
Nombre de favoris 0

A Forum Numerica seminar
by Luca Padovani (University of Camerino, Italy)

Abstract:

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.

Speaker's Bio:
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.

FORUM NUMERICA is sponsored by the Academy of Excellence “Networks, Information and Digital Society” of UCAJEDI
More information here: https://ds4h.univ-cotedazur.eu/forum-numerica

Mots clés : ds4h forum numerica

Commentaire(s)