Typage et Programmation

Ces notes sont le support du cours Typage et Programmation que j'ai dispensé avec Michel Mauny et Xavier Leroy dans le cadre du D.E.A. Sémantique, Preuves et Programmation.

Résumé

Le but de ce cours est de montrer l'apport du typage dans les langages de programmation, et de présenter les méthodes et techniques de base pour l'étude des langages fortement typés.

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 ).


Examens

  1. Sujet avec corrige question par question