Séminaire en ligne, 20 janvier 2022
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é 11h45: 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:15 – 11:30
-
Bruno Dinis (Universidade de Lisboa, Portugal)Invited talk: Functional interpretations and applications
Functional interpretations are maps of formulas from the language of one theory into the language of another theory, in such a way that provability is preserved. These interpretations typically replace logical relations by functional relations. Functional interpretations have many uses, such as relative consistency results, conservation results, and extraction of computational content from proofs as is the case in the so-called proof mining program.
I will present several recent functional interpretations and some results that come from these interpretations. I will also give examples of application of functional interpretations, in the spirit of the proof mining program.
