Formalisation mathématique et types dépendants : Le point vue d'un utilisateur mathématicien
Apparaît dans la collection : Workshop Schlumberger : Types dépendants et Formalisation des mathématiques
Dans cet exposé je passerai en revue les surprises bonnes et moins bonnes je j'ai rencontrées en formalisant des mathématiques modernes en théorie des types dépendants.
