Appears in collection : Workshop Schlumberger : Types dépendants et Formalisation des mathématiques
What can be done when formalising 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 formalising Grothendieck's schemes using only Isabelle's module system called "locales".
By Pierre Vanhove
By Pierre Vanhove
By Misha Gromov
By Céline Duval
By Olivier Benoist
