Name: Workshop Schlumberger : Types dépendants et Formalisation des mathématiques
Start: 2022-06-15T09:00:00+02:00
End: 2022-06-15T18:30:00+02:00
Location: Le Bois-Marie

Workshop Schlumberger : Types dépendants et Formalisation des mathématiques

Wednesday, June 15, 2022 - 9:00 AM

Monday, June 13, 2022
Tuesday, June 14, 2022
Wednesday, June 15, 2022

9:00 AM Café d'accueil
Café d'accueil
9:00 AM - 9:30 AM
Room: Centre de conférences Marilyn et James Simons
9:30 AM Formalisation mathématique et types dépendants : Le point vue d'un utilisateur mathématicien (T: 45min + Q: 15) - Patrick MASSOT (LMO, Université Paris-Saclay)
Formalisation mathématique et types dépendants : Le point vue d'un utilisateur mathématicien (T: 45min + Q: 15)
- Patrick MASSOT (LMO, Université Paris-Saclay)
9:30 AM - 10:30 AM
Room: Centre de conférences Marilyn et James Simons Dans cet exposé je passerai en revue les surprises bonnes et moins bonnes je j'ai rencontrées en formalisant des mathématiques modernes en théorie des types dépendants.
10:30 AM Pause café
Pause café
10:30 AM - 11:00 AM
Room: Centre de conférences Marilyn et James Simons
11:00 AM How to Do Maths Without Dependent Types (T: 45 min + Q: 15min) - Anthony BORDG (University of Cambridge)
How to Do Maths Without Dependent Types (T: 45 min + Q: 15min)
- Anthony BORDG (University of Cambridge)
11:00 AM - 12:00 PM
Room: Centre de conférences Marilyn et James Simons What can be done when formalizing mathematics without dependent types? I will give you new insights into this question by exploring the capability and possible limitations of the Isabelle/HOL proof assistant. I will explain what we learnt formalizing Grothendieck's schemes using only Isabelle's module system called "locales".
12:00 PM Déjeuner
Déjeuner
12:00 PM - 1:30 PM
Room: Centre de conférences Marilyn et James Simons
1:30 PM Functional Encodings of Mathematics (T: 45 min + Q: 15min) - Georges GONTHIER (INRIA)
Functional Encodings of Mathematics (T: 45 min + Q: 15min)
- Georges GONTHIER (INRIA)
1:30 PM - 2:30 PM
Room: Centre de conférences Marilyn et James Simons A remarkable feature of logics based on typed lambda calculus is that they allow embedding functional programs in the representation of mathematical knowledge. These can be used to animate formal theories and make them behave, in part, as a working mathematician would expect. Examples of such functional encodings have played a key part in several large formal proofs, such as this of the Four-Color and Odd Order theorems.
2:30 PM Verified Computational Mathematics (T: 45min + Q: 15min) - Assia MAHBOUBI (INRIA)
Verified Computational Mathematics (T: 45min + Q: 15min)
- Assia MAHBOUBI (INRIA)
2:30 PM - 3:30 PM
Room: Centre de conférences Marilyn et James Simons Computers are widely used as observation instruments for testing and refining conjectures, in a broad range of mathematical areas. They actually even substantiate actual proof steps in published proofs. In particular, a large class of computer proofs today involve symbolic computations, often produced by computer algebra systems. While these systems have become amazingly efficient, they also tend to exhibit awkward behaviors on seemingly innocuous queries. This talk will discuss the challenges raised by the formal verification of symbolic computation, and the potential of proof assistants based on dependent types.
3:30 PM Pause café
Pause café
3:30 PM - 4:00 PM
Room: Centre de conférences Marilyn et James Simons
4:00 PM Le principe d'univalence: le transfer du raisonnement à travers les equivalence (T: 45min + Q: 15min) - Benedikt AHRENS (Delft University of Technology)
Le principe d'univalence: le transfer du raisonnement à travers les equivalence (T: 45min + Q: 15min)
- Benedikt AHRENS (Delft University of Technology)
4:00 PM - 5:00 PM
Room: Centre de conférences Marilyn et James Simons Le raisonnement à équivalence près est omniprésent en mathématique, et les mathématiciens le font implicitement. Pour les mathématiques sur ordinateurs, ce n'est pas si simple : il faut donner tous les détails explicitement. C'est pour cela que Voevodsky a créé les fondements univalents, avec l'objectif de mécaniser le transfer du raisonnement à travers les équivalences. Je présenterai notre travail (avec North, Shulman et Tsementzis) sur le principe d'univalence en fondements univalents, qui met en pratique la vision de Voevodsky.
5:00 PM Hierarchy Builder (T: 45min + Q: 15min) - Cyril COHEN (INRIA)
Hierarchy Builder (T: 45min + Q: 15min)
- Cyril COHEN (INRIA)
5:00 PM - 6:00 PM
Room: Centre de conférences Marilyn et James Simons Libraries of machine-checked code are, nowadays, organized around hierarchies of algebraic structures. Unfortunately, the language of Type Theory and the features provided by modern proof assistants make the construction of a hierarchy hard even for expert users. The difficulty begins with the non-orthogonal choices, between storing information as record fields or parameters, and between different inference mechanisms. To this, one may add the concerns about performance and about the usability, by a non-expert, of the final hierarchy. Hierarchy Builder (HB), as implemented inside the Coq proof assistant, gives library designers a language to describe the building blocks of algebraic structures and to assemble them into a hierarchy. Similarly, it provides the final user tools to build instances of structures and to inform the system how to take advantage of this knowledge during type inference. Finally, HB lets library designers improve the usability of their library by providing alternative interfaces to the primitive ones, a feature that is also useful to accommodate changes to the hierarchy without breaking user code. This is joint work with Kazuhiko Sakaguchi and Enrico Tassi.