How to Do Maths Without Dependent Types (T: 45 min + Q: 15min)

Jun 15, 2022, 11:00 AM
1h
Centre de conférences Marilyn et James Simons (Le Bois-Marie)

Centre de conférences Marilyn et James Simons

Le Bois-Marie

35, route de Chartres 91440 Bures-sur-Yvette

Speaker

Prof. Anthony BORDG (University of Cambridge)

Description

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".

Presentation materials