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.
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:
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).
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ç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 (et vous pouvez avoir les sources Tex en suivant ce lien).
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).
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).
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.
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).
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
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
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.
Trouver une propriété P pour que le triplet
{P}soit prouvable avec les règles de la logique de Hoare. Construisez la dérivation.x:=x+y; y:= y+2x {y=3x}
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
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}
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 nous avons étudié les exercices relatifs au calcul de pré-condition la plus faible des examens des années précédentes:
Construisez un programme de quelques lignes
qui suppose en entrée que la variable
D'autres exercices sont proposés dans ce lien (merci à Marieke Huisman).
Mars 2005, correction, Janvier 2002, correction, Janvier 2001, correction