Séminaire en ligne, 17 juin 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
-
Sonia Marin (University College London)
Focusing is a general technique for syntactically compartmentalising the non-deterministic choices in a proof system, which not only improves proof search but also has the representational benefit of distilling sequent proofs into synthetic normal forms. However, since focusing was traditionally specified as a restriction of the sequent calculus, the technique had not been transferred to logics that lack a (shallow) sequent presentation, as is the case for some modal or substructural logics.
With K. Chaudhuri and L. Straßburger, we extended the focusing technique to nested sequents, a generalisation of ordinary sequents which allows us to capture all the logics of the classical and intuitionistic S5 cube in a modular fashion. This relied, following the method introduced by O. Laurent, on an adequate polarisation of the syntax and an internal cut-elimination procedure for the focused system which in turn is used to show its completeness.
Recently, with A. Gheorghiu, we applied a similar method to the logic of Bunched Implications (BI), a logic that freely combines intuitionistic logic and multiplicative linear logic. For this we had first to reformulate the traditional bunched calculus for BI using nested sequents, followed by a polarised and focused variant that (again) we show is sound and complete via a cut-elimination argument.
