Formalisation mathématique et types dépendants : Le point vue d'un utilisateur mathématicien
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.