

Formalisation mathématique et types dépendants : Le point vue d'un utilisateur mathématicien
By Patrick Massot


Le principe d'univalence: le transfer du raisonnement à traver les equivalence
By Benedikt Ahrens
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".