Séminaire en ligne, 22 avril 2021

Pour assister à la rencontre, se rendre sur https://ent-services.ens-lyon.fr/entVisio/ choisir Chocola dans le menu déroulant, mettre son nom comme identifiant, et Bruxelles sans majuscule comme dernier champ. Autoriser les popups, et changer de navigateur au besoin.

10h: accueil et problèmes de connexion 10h15: début de l'exposé 11h15: questions et discussion 12h: adieu et problèmes de déconnexion Merci aux auditeurs de couper micro et caméra (sauf éventuellement, lorsqu'ils souhaitent poser une question). Les questions peuvent aussi être posées dans la fenêtre de chat.

En cas de problème ou de question, écrire à chocola-gestion chez ens-lyon.fr.

Programme

10:00 – 12:00
Gabriele Vanoni (Università di Bologna)

Girard's Geometry of Interaction (GOI) can be made concrete by considering it as an implementation technique for functional programs, in particular the lambda calculus. Our work is about the complexity analysis of the abstract machine based on the GOI, the interaction abstract machine (IAM). We have adapted in a non trivial way de Carvalho's non idempotent intersection types so that type derivations completely characterize the time and space complexity of the IAM, thus providing a logical account of the IAM resource usage. Moreover, by the way of the type systems we have introduced, we are able to state some negative results about time and space cost models for the lambda calculus based on the IAM. This is joint work with Beniamino Accattoli and Ugo Dal Lago.