Le 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, 2001-2002, 2002-2003,et en 2003-2004.
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
Voici l'exercice concernant le lambda-calcul pur du dernier examen.
Un chercheur lunatique et obstiné décide de représenter les valeurs booléennes de la fa\c{c}on suivante:
F = lambda x y. x
T = lambda x y. y
Comment doit-il alors choisir la valeur de IF pour qu'elle ait le comportement usuel d'une expression conditionnelle?
Notre chercheur veut maintenant représenter les listes, il se donne la représentation suivante:
Cons = lambda x y z. z x y
Nil = lambda x. x
Quelle sont les formes normales des deux listes contenant un seul élément qui est respectivement F et T?
Il propose ensuite les valeurs suivantes pour la fonction VIDE qui permet de distinguer une liste vide d'une liste non vide. Lesquelles de ces valeurs sont-elles adaptées?
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.
On considère que les types t1, t2, t3 et t4 sont des types de base. Fournir des termes ayant les types suivants:
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:
Construire une dérivation de sémantique naturelle pour l'exécution des programmes suivants dans l'environnement initial (x,1).(y,2).[]
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 dans les notes de cours
{n >= 0}
k = 0;
a = 0;
b = 1;
while (k <> n) {
{invariant: 2 * a = k^3 + k & 2 * b = 3 * k^2 - 3 * k + 2}
b = b + 3 * k;
a = a + b;
k = k + 1;
}
{2 * a == n^3 + n}
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