Séminaire

Équipe-projet Inria Picube (Inria)


Jour, heure et lieu

Le lundi à 14h, 1007 ou 3052

Le calendrier des séances (format iCal).
Pour ajouter le calendrier des séances à votre agenda favori, souscrire au calendrier en indiquant ce lien.


Contact(s)

Le séminaire Formath (Formalized mathematics) est le séminaire de l'équipe Picube.

Pour s'abonner à la liste de diffusion, consulter la page https://listes.irif.fr/sympa/info/formath ou écrire aux responsables du séminaire.


Formath
Lundi 3 avril 2023, 14 heures, 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
Lundi 17 avril 2023, 14 heures, TBA
Arthur Charguéraud (Camus team, ICPS, iCube, INRIA) Non encore annoncé.

Formath
Mardi 9 mai 2023, 0 heures, TBA
Louise Dubois De Prisque (LSV, CNRS & ENS Paris-Saclay) Non encore annoncé.



Année 2023

Formath
Lundi 20 mars 2023, 15 heures, 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é.