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, 2003-2004,et en 2004-2005.

Cours de sémantique (année 2005-2006)

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 et 8 séances de travaux dirigés sur machine.

Dans tous les cas, je vous conseille la littérature suivante:

  1. Une très bonne introduction au lambda-calcul est fournie dans cet article de H. Barendregt and E. Barendsen, Introduction to Lambda Calculus, 1994
  2. Une introduction à Coq par moi-même: Coq in a Hurry
  3. ,
  4. Il y a un très bon livre de Hanne Riis Nielson et Flemming Nielson Semantics with Applications, a formal introduction, Wiley, 1992.
  5. Glynn Winskel, The Formal semantics of Programming Languages, An Introduction, MIT Press, 1993

Première séance: le lambda-calcul pur

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

TD de la première séance

Dans ces travaux dirigés, nous étudierons les exercices donnés dans les notes de cours

Devoir à la maison pour la première séance

Voici l'exercice concernant le lambda-calcul pur du dernier examen.

  1. Un chercheur lunatique et obstiné décide de représenter les valeurs booléennes de la faç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?

  2. 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?

    1. lambda z. z T F
    2. lambda l. l (lambda x y z. z)(lambda x. x)(lambda x. F) T
    3. lambda l. l (lambda x y z. z)(lambda x y. T) F F
    4. lambda l. l (lambda x y. F)
  3. Deuxième séance: le lambda-calcul pur

    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.

    TD de la deuxième séance

    Dans ces travaux dirigés, nous continuons avec les exercices des notes de cours de la première séance.

    Troisième séance: le lambda-calcul typé

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

    TD de la troisième séance

    On fera les exercices donnés en suivant ce lien.

    Devoir à la maison pour la troisième séance

    On considère que les types t1, t2, t3 et t4 sont des types de base. Fournir des termes ayant les types suivants:

    1. (t1->t2->t3->t4)->(t1->t2)->(t2->t3->t4)->(t2->t3)->t1->t4
    2. (t2->t1)->(t1->t0)->(t2->t1->t0)
    3. (t1->t3)->(t2->t1)->(t3->t1->t4)->t1->t4

    Quatrième séance: la sémantique naturelle

    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 (et vous pouvez avoir les sources Tex en suivant ce lien).

    TD de la quatrième séance

    Dans les TD nous avons étudié le codage des descriptions sémantiques en Coq et nous observé une dérivation de sémantique naturelle sous sa forme théorique et sous sa forme Coq. Ensuite, nous avons fait des exercices pris dans ce document (suivre ce lien pour avoir les sources Tex de ce fichier) et le fichier Coq correspondant.

    Si vous voulez construire vos propres documents électroniques contenant des dérivations de sémantique naturelle, je suggère que vous regardiez comment c'est fait dans les sources des notes de cours (pas terrible), ou que vous modifiiez le fichier suivant avec OpenOffice Draw (le même fichier au format svg, ou format pdf).

    Devoirs à la maison pour la quatrième séance

    Construire une dérivation de sémantique naturelle pour l'exécution des programmes suivants dans l'environnement initial (x,1).(y,2).[] (j'utilise [] pour représenter l'environnement vide).

    Cinquième séance: la sémantique dénotationnelle

    Dans ce cours nous présentons une autre description du petit langage impératif utilisé comme exemple pour le cours précédent. Les notes de cours sont disponibles en suivant ce lien. On trouve également un développement Coq associé, où le théorème de Tarski est démontré à partir des axiomes de base de la logique classique et où ce théorème est ensuite utilisé pour produire la fonction qui représente la sémantique dénotationnelle des instructions. Une preuve mécanisée de correction de la fonction est également jointe.

    TD de la cinquième séance

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

    Sixième séance: Les ordres partiels complets

    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.

    TD de la sixième séance

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

    Devoirs à la maison pour la sixième séance

    Ce devoir a été déposé le 13 Mars au matin. Il est à faire pour le 20 mars au soir.

    Soit S l'ensemble {1,2,3,4}, nous noterons bottom un objet qui n'est pas dans S et nous considérerons la fonction F de type(S -> S union {bottom})->(S->S union {bottom}).

    F(g,i) = si i = 1 alors g(2)
             si i = 2 alors g(4)
             si i = 3 alors g(3)
             si i = 4 alors 1
    
    1. Donnez, in extenso, les valeurs prises par les fonctions F, F2, F3, F4.
    2. Donnez, in extenso, les valeurs prises par le plus petit point fixe de F.

    Septième séance: Sémantique axiomatique

    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.

    TD de la septième séance

    Premier exercice

    Trouver une propriété P pour que le triplet

    {P}x:=x+y; y:= y+2x{y=3x}
    
    soit prouvable avec les règles de la logique de Hoare. Construisez la dérivation.

    En raisonnant sur l'invariant de boucle, trouvez une précondition P, pour que la post-condition y=n3 soit satisfaite après l'exécution du programme suivant:

    while(x < n) do
      x := x+1;
      y := y+z;
      z := z+t;
      t := t+u;
    done
    

    Devoirs à la maison pour la septième séance

    Trouvez des constantes a, b, c pour que le triplet de Hoare suivant soit dérivable. Construisez la dérivation.

    {x = 0 /\ y = a /\ z = b /\ t = c}
    while (x < n) do
      x := x+1;
      y := y+z;
      z := z+t;
    done
    {y=n2+3n}
    

    Huitième séance: Calcul de préconditions

    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.

    TD de la huitième séance

    Dans cette séance nous avons étudié les exercices relatifs au calcul de pré-condition la plus faible des examens des années précédentes:

    Premier exercice

    Construisez un programme de quelques lignes qui suppose en entrée que la variable x contient une valeur positive ou nulle, qui modifie éventuellement plusieurs variables différentes de x et qui termine dans un état où y est la racine cubique de x. Annotez ce programme de façon à exprimer ces conditions et les invariants de boucle utilisés. Indiquez quelles sont les conditions de vérification engendrées pour ce programme. On préférera, si c'est possible, une solution qui n'effectue que des additions.

    D'autres exercices sont proposés dans ce lien (merci à Marieke Huisman).

    Examens des années précédentes

    Mars 2005, correction, Janvier 2002, correction, Janvier 2001, correction


    Yves Bertot
    Last modified: Mon Sep 5 08:32:37 MEST 2005