A gentle introduction to template games and linear logic
By Paul-André Melliès
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.