Types dépendants dans les langages de programmation

Cette séance de cours couvre différents types de cartes, opérateurs de type, équivalence de types, opérateurs de type de première classe, syntaxe et sémantique du système Fw, équivalence de type, calcul des constructions, systèmes de types purs, cube lambda, types dépendants dans Coq, univers de type dans Coq, définitions inductives et récursion dans Coq, correspondance Curry-Howard et équivalence entre LEM et DNE. Il traite également du problème de la vérification de type dans les langages de programmation et de l'adoption des types dépendants dans Scala et Haskell.