Nous prendrons comme exemple le langage ML et quelques extensions (structures mutables, types enregistrements, sous-typage). Nous décrirons en détail son système de typage et les algorithmes de synthèse de types, nous définirons formellement l'évaluation, puis nous montrerons comment le typage garantit la sécurité de l'évaluation, tout en insistant sur l'aspect modulaire du formalisme. Nous étudierons également l'ajout d'un système d e modules à un langage fortement typé.
Vous pouvez retirer les notes complètes au format postscript (compressé) ou au format dvi (compressé). Vous pouvez aussi les consulter par chapitre (La rédaction du chapitre 8 est inachevée; suite à plusieurs, j'ai décidé de la distribuer dans son état provisoire, et malheureusement encore assez brouillon ).