Summer school "Proof assistants and applications"
from
Monday, 31 August 2026 (09:00)
to
Friday, 4 September 2026 (19:50)
Monday, 31 August 2026
09:00
Introduction to type theory: L. Pujet (L1)
L. Pujet (L1)
09:00 - 10:30
Room: Salle de conférences
10:30
Coffee break
Coffee break
10:30 - 11:00
Room: Salon
11:00
Introduction to transformers and their application to proof assistants: T. Stoskopf (L1)
T. Stoskopf (L1)
11:00 - 12:30
Room: Salle de conférences
14:00
Introduction to categorical logic: T. Benjamin (L1)
T. Benjamin (L1)
14:00 - 15:30
Room: Salle de conférences
15:30
Coffee break
Coffee break
15:30 - 16:00
Room: Salon
16:00
Introduction to type theory: L. Pujet (P1)
L. Pujet (P1)
16:00 - 17:00
Room: Salle de conférences
Tuesday, 1 September 2026
09:30
Introduction to type theory: L. Pujet (L2)
L. Pujet (L2)
09:30 - 11:00
Room: Salle de conférences
11:00
Coffee break
Coffee break
11:00 - 11:30
Room: Salon
11:30
Introduction to type theory: L. Pujet (P2)
L. Pujet (P2)
11:30 - 12:30
Room: Salle de conférences
14:00
Introduction to synthetic homotopy theory: A. Ljungström (L1)
A. Ljungström (L1)
14:00 - 15:30
Room: Salle de conférences
15:30
Coffee break
Coffee break
15:30 - 16:00
Room: Salon
16:00
Introduction to synthetic homotopy theory: A. Ljungström (P1)
A. Ljungström (P1)
16:00 - 17:00
Room: Salle de conférences
Wednesday, 2 September 2026
09:00
Introduction to transformers and their application to proof assistants: T. Stoskopf (L2)
T. Stoskopf (L2)
09:00 - 10:30
Room: Salle de conférences
10:30
Coffee break
Coffee break
10:30 - 11:00
Room: Salon
11:00
Introduction to Lean: Formalizing Mathematics with Mathlib: X. Roblot
X. Roblot
11:00 - 12:30
Room: T04
14:00
Introduction to transformers and their application to proof assistants: T. Stoskopf (P1)
T. Stoskopf (P1)
14:00 - 16:00
Room: T04
16:00
Coffee break
Coffee break
16:00 - 16:30
Room: Salon
16:30
Numerical Computations and Proofs, from Proof-Assistants to Aerospace Applications: P. Roux (talk)
Numerical Computations and Proofs, from Proof-Assistants to Aerospace Applications: P. Roux (talk)
16:30 - 17:30
Room: Salle de conférences
Thursday, 3 September 2026
09:00
Introduction to categorical logic: T. Benjamin (L2)
T. Benjamin (L2)
09:00 - 10:30
Room: Salle de conférences
10:30
Coffee break
Coffee break
10:30 - 11:00
Room: Salon
11:00
Introduction to Lean: Formalizing Mathematics with Mathlib: X. Roblot (L2)
X. Roblot (L2)
11:00 - 12:30
Room: T04
12:30
Cocktail
Cocktail
12:30 - 14:00
Room: Salon
14:00
Introduction to categorical logic: T. Benjamin (P)
T. Benjamin (P)
14:00 - 16:00
Room: Salle de conférences
16:00
Coffee break
Coffee break
16:00 - 16:30
Room: Salon
16:30
High-assurance and high-speed cryptography with Jasmin and EasyCrypt: J.-C. Léchenet (talk)
High-assurance and high-speed cryptography with Jasmin and EasyCrypt: J.-C. Léchenet (talk)
16:30 - 17:30
Room: Salle de conférences
Friday, 4 September 2026
09:30
Introduction to synthetic homotopy theory: A. Ljungström (L2)
A. Ljungström (L2)
09:30 - 11:00
Room: Salle de conférences
11:00
Coffee break
Coffee break
11:00 - 11:30
Room: Salon
11:30
Introduction to synthetic homotopy theory: A. Ljungström (P2)
A. Ljungström (P2)
11:30 - 12:30
Room: Salle de conférences
14:00
Introduction to Lean: Formalizing Mathematics with Mathlib: X. Roblot (P)
X. Roblot (P)
14:00 - 16:00
Room: T04
16:00
Coffee break
Coffee break
16:00 - 16:30
Room: Salon
16:30
Introduction to transformers and their application to proof assistants: T. Stoskopf (P2)
T. Stoskopf (P2)
16:30 - 17:30
Room: T04