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