Seminar

Inria project-team Picube (Inria)


Day, hour and place

Monday at 2:00pm, room 1007 or 3052

The calendar of events (iCal format).
In order to add the event calendar to your favorite agenda, subscribe to the calendar by using this link.


Contact(s)


Formath
Monday April 3, 2023, 2PM, 1007
Olivier Laurent (Équipe Plume, Laboratoire de l'Informatique du Parallélisme (LIP), ENS Lyon) 1, 2, 3, Yalla: Linear Logic in Coq

We discuss the formalization of Linear Logic, through the development of the Yalla library for Coq:

https://perso.ens-lyon.fr/olivier.laurent/yalla/

The initial specification was to get a library which:

  • would provide standard results on the proof theory of Linear Logic;
  • could be reused, thus in particular able to deal with some variants of the system;
  • should be compatible with the Curry-Howard interpretation of proofs, thus faithful to their computational content.

We will describe the evolution of the project and how it matches this specification through the different versions of the library: Yalla 1, Yalla 2 (current version), Yalla 3 (future directions).

Following all previous known works, Yalla 1 defined proofs in Prop. It relies on an explicit exchange rule for dealing with the computational content of proofs. Yalla 2 corresponds to a move to Type to be able to extract computational informations from proofs. Yalla 3 will rely on a different way of approaching exchange to be able to deal with local transformations of proofs more easily.

Formath
Monday April 17, 2023, 2PM, TBA
Arthur Charguéraud (Camus team, ICPS, iCube, INRIA) To be announced.

Formath
Tuesday May 9, 2023, 0AM, TBA
Louise Dubois De Prisque (LSV, CNRS & ENS Paris-Saclay) To be announced.



Year 2023

Formath
Monday March 20, 2023, 3PM, 1007
Riccardo Brasca (IMJ-PRG, Université Paris-Cité) Le dernier théorème de Fermat pour les premiers réguliers en Lean

Le dernier théorème de Fermat est un résultat en théorie des nombres qui a été conjecturé en 1637, mais qui a été démontré seulement en 1995. La démonstration repose sur des techniques mathématiques modernes et sa formalisation est actuellement hors de portée. Dans cet exposé je vais expliquer la formalisation en Lean d'un cas particulier de ce théorème, où l'on suppose que l'exposant est un nombre premier “régulier” (cette notion sera introduite pendant l'exposé). Je vais aussi décrire l'assistant de preuve Lean et sa bibliothèque mathématique mathlib, et j'expliquerai l'intérêt mathématique d'un tel projet. Aucune connaissance en théorie de nombres est nécessaire pour suivre l'exposé.