 | Page principale | Dernière modification : 10 August 2021 |
Jusqu'en 2009-2010, j'ai enseigné, en collaboration avec Giuseppe Castagna et Didier Rémy, le cours 2-4-2 du MPRI.
Cette page reste en l'état et propose diverses ressources datant des années 1999 à 2010.
À partir de 2017-2018, je participe à nouveau au cours 2-4 du MPRI.
Mon objectif est principalement de décrire le système de types de Hindley et Milner, qui sert de fondation aux langages de programmation de la famille ML, dont Standard ML, OCaml et Haskell. Je présenterai ce système de types, son algorithme d'inférence de types, ainsi qu'un certain nombre de leurs extensions. Je consacrerai également un certain temps à des techniques de compilation préservant le typage.
En 2006-2007 et 2007-2008, Xavier Leroy a participé à ce cours; ses transparents sont toujours en ligne.
L'évaluation des étudiants s'effectue pour partie via un partiel et un examen écrits, pour partie via un projet de programmation.
Le cours ne s'appuie pas explicitement sur un texte particulier. En particulier, le plan du cours ne correspond exactement à aucune des références bibliographiques que je propose. Néanmoins, celles-ci constituent un bon accompagnement au cours.
J'ai écrit début 2007 un embryon de nouvelles notes de cours dans lesquelles, pour l'instant, on ne trouve pas grand-chose, si ce n'est la démonstration du lemme de stabilité du typage par substitution (de types pour des variables de types), écrite en accordant une attention particulière aux arguments de renommage.
À ceux que le typage intéresse, je recommande fortement la lecture de tout ou partie de l'ouvrage Types and Programming Languages (TAPL), de Benjamin C. Pierce. Ce livre est accessible et très complet. En particulier, l'équivalent des chapitres 1 à 14 (lambda-calcul simplement typé) et 22 (inférence de types) sera soit supposé connu soit traité en cours.
Nous aborderons également en cours plusieurs sujets absents de TAPL: en particulier, l'inférence de types à la ML (donc avec polymorphisme) et l'inférence de types à base de contraintes. Le second chapitre de mon mémoire d'habilitation (HDR) constitue une brève introduction à ces questions. Ensuite, pour approfondir, on pourra se plonger dans The Essence of ML Type Inference (EMLTI). Ce chapitre, écrit par Didier Rémy et moi-même, est paru dans Advanced Topics in Types and Programming Languages. Il contient une présentation assez détaillée du système de types du langage ML, et s'attache à décrire de façon élégante un algorithme efficace d'inférence de types.
Je n'aurai pas le temps d'aborder en cours deux aspects importants du langage OCaml, à savoir le système de modules et le système de classes et objets. Tous deux sont décrits dans les notes de cours de Didier Rémy, intitulées Using, Understanding, and Unraveling the OCaml Language, dont je conseille la lecture. On peut également se référer aux articles qui décrivent de façon formelle l'essentiel de ces systèmes, à savoir A Modular Module System, de Xavier Leroy, en ce qui concerne les modules, et Objective ML: An effective object-oriented extension to ML, de Didier Rémy et Jérôme Vouillon, en ce qui concerne les classes et objets.
Les notes de cours de DEA de l'année 2002-2003 sont encore disponibles, pour ceux que cela intéresserait, mais ne seront plus mises à jour. Vous pouvez consulter le code correspondant aux exercices de programmation des chapitres 1, 2, 3, 5, et 6, ainsi que celui correspondant à l'algorithme d'unification du chapitre 7.
2006-2007 était un bon cru.
| Page principale | Dernière modification : 10 August 2021 |