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