e plan du cours change d'année en année. Vous pouvez accéder au cours tel que je l'avais fait (ou avais prévu de le faire) en 2000-2001 et en 2001-2002.
L'objectif de ce cours est d'introduire les étudiants aux différentes techniques utilisées pour décrire exactement le comportement des programmes. Ce cours est organisé en 8 séances de 2 heures, accompagnées de 8 séances de Travaux dirigés sur machine.
Dans ce cours nous présentons le lambda-calcul pur, en le voyant comme un langage de programmation minimal. Nous montrons les difficultés de l'alpha-conversion, le pouvoir expressif du langage, et les propriétés de confluence. Ceci permet en particulier de distinguer les langages paresseux. Les notes de ce cours sont disponibles ici (en postscript compressé).
Dans ces travaux dirigés, nous étudierons les exercices donnés dans les notes de cours
Dans ce cours nous continuons la présentation du lambda-calcul pur, en particulier en étudiant les propriétés de terminaison et de stratégie d'évaluation.
Dans ces travaux dirigés, nous continuons avec les exercices des notes de cours de la première séance.
Dans ce cours nous présentons le typage simple du lambda-calcul. Nous voyons sans les démontrer certaines des propriétés des types: conservation des types à l'exécution, terminaison forte. Nous abordons ensuite l'inférence de type et le typage polymorphe. Ce cours est aussi une occasion pour ré-introduire l'utilisation de règles d'inférence (comme en logique). Les notes de cours sont disponibles ici (en postscript compressé).
On fera les exercices donnés en suivant ce lien.
Dans ce cours on présente la description d'un petit langage impératif dans le style de la sémantique naturelle. Les notes de ce cours sont disponibles en suivant ce lien
Les TD de la quatrième séance continuent sur le thème du lambda-calcul, pur ou typé, en utilisant caml (langage fonctionnel typé) pour décrire un réducteur de termes du lambda-calcul pur.
Ce TD repose sur deux fichiers ML, dont l'un est à compléter dans
Il s'agit d'effectuer les travaux suivant:
Dans ce cours nous présentons encore la description du petit langage impératif utilisé comme exemple pour la sémantique naturelle. Les notes de cours sont disponibles en suivant ce lien.
Dans cette séance, on fera les exercices proposés dans le cours de sémantique naturelle (en particulier les exercices 1, 2, 4, 5, 6, 7, 8, 9).
Dans ce cours nous apportons des précisions sur les structures mathématiques utilisées en sémantique dénotationnelle. Les notes de cours sont disponibles en suivant ce lien.
Dans cette séance, on fera les exercices proposés dans le cours de sémantique dénotationnelle (en particulier les exercices 1, 2, 3, 7, 9, 10).
Dans ce cours nous étudions un jeu de règles de raisonnement qui permettent de raisonner sur les programmes. Les notes de ce cours sont disponibles en suivant ce lien ce lien.
Dans cette séance on fera les exercices proposés en suivant ce lien.
Dans ce cours nous étudions le prolongement de la sémantique axiomatique qui permet de calculer les formules logiques qui doivent être satisfaites pour qu'un programme soit cohérent avec les annotations logiques qu'il comporte. Les notes de cours sont les mêmes que pour le cours précédent.
Dans cette séance, on fera les exercices proposés en suivant ce lien (merci à Marieke Huisman).
Janvier 2002, correction, Janvier 2001, correction