Théorie de la Programmation - L3IF      


Cours assuré par Daniel Hirschkoff
Chargés de TDs/TPs: Julien Braine, Adrien Durier, Alexis Ghyselen


Transparents du cours disponibles ici (à noter que l'essentiel du cours est donné au tableau).
Une version imprimable des transparents (avec moins d'illustrations).
Fichiers pour les TPs.


DM1 à rendre le 2 octobre
DM1bis à rendre le 9 octobre
Le partiel aura lieu mercredi 24 octobre, de 8h à 10h, en amphi B (sur le créneau du TD). Seuls les documents sur papier sont autorisés (notes de cours/TD/TP, livres).
   Voici un exemple de sujet de partiel tiré du passé, avec DM dont il est question dans le sujet.
DM2 à rendre le 18 décembre, au début du cours (ici le même sujet en version lambda-calcul, si vous préférez)

DateCours
11/09 . introduction,
. grammaire de IMP
. esquisse de sémantique . dénotationnelle (Winskel, section 5.2)
. sémantique opérationnelle à petits pas, début
   - Sections 1 et 2 des notes de Harvard (petits pas pour les expressions arithmétiques)
   - pages 12 à 16 des notes de P. Sewell -- attention, la grammaire de IMP diffère un peu : il y a !l, et, surtout, la grammaire est à plat (juste des expressions)
18/09 . petits pas pour IMP, suite (la photo)
. introduction à Coq (fichiers)
25/09 . théorème de Knaster-Tarski
. définitions inductives d'ensembles
. preuves par induction structurelle
   - fichier Coq vu en cours
   - notes sur la forme générale des définitions inductives et les preuves par induction
   - Section 3.1 des notes de P. Sewell -- comme indiqué ci-dessus, la grammaire de IMP diffère; et ne soyez pas effrayés par la preuve détaillée
   - des notes sur définitions inductives et points fixes
02/10 . grands pas pour Imp
. définitions inductives de relations n-aires
. preuves par induction sur la dérivation
   - fichier Coq vu en cours
   - Section 3.2 des notes de P. Sewell -- vous pouvez ignorer ce qui concerne le typage (relation notée |- )
   - la partie correspondante dans le cours à UPenn
09/10 . alerte incendie (!)
. (éléments de) correction du DM 1bis
. logique de Floyd-Hoare : introduction
. définitions de base : (pré-)assertions, satisfaction, validité
. règles de la logique de Hoare
   - chapitre 6 dans le livre de G. Winskel ; une version abrégée du contenu de ce chapitre est proposée à Harvard ;
     le traitement des assertions dans le cours est pour le moment plus simple, puisqu'on a présenté les pré-assertions
   - la partie correspondante dans le cours à UPenn (les assertions sont représentées comme un type Coq approprié)
16/10 . logique de Floyd-Hoare : retour sur les règles d'inférence
. exemple de programme annoté
. correction de la logique de Hoare
. quelques mots sur la complétude
   - références : les mêmes que pour la séance précédente
23/10 . fin de la logique de Floyd-Hoare : assertions, quantificateurs, lieurs, alpha-conversion
. retour sur la sémantique dénotationnelle de IMP : domaines, théorème du point fixe
   - références : le livre de G. Winskel (partie 6.2) pour les assertions en logique de Floyd-Hoare
   - pour la sémantique dénotationnelle de IMP, le livre de G. Winskel (parties 5.1 à 5.4), le cours à Harvard
6/11 . systèmes de réécriture abstraite, systèmes de réécriture de mots
. terminaison, caractérisation via le principe d'induction bien fondée (2.2), utilisation aquatique de l'induction bien fondée
. établir la terminaison : mesure, produit lexicographique (2.4), extension multiensemble (2.5)
   - références : le livre de F. Baader et T. Nipkow, "Term Rewriting and All That", qui est disponible à la bibliothèque. Les indications entre parenthèses ci-dessus font références à des parties du chapitre 2 de ce livre.
13/11 . terminaison pour les systèmes de réécriture de mots
. confluence dans les systèmes de réécriture abstraite, Lemme de Newman
. paires critiques pour les systèmes de réécriture de mots
. termes, substitutions : définitions, notations (3.1)
20/11 . unification du premier ordre : algorithme, correction et complétude (4.5, 4.6)
. systèmes de réécriture de termes : définition (4.2)
27/11 . petit langage fonctionnel : syntaxe, liaison et alpha-conversion, grands pas, petits pas, exemples, liens avec le lambda-calcul
   - éventuellement le chapitre 11 du livre de G. Winskell, mais celui-ci va bien plus loin que le cours
   - Sections 4.1 et 4.2 des notes de P. Sewell -- vous pouvez ignorer ce qui concerne le typage (relation notée |- )
   - la partie correspondante dans le cours à UPenn
04/12 . retour rapide sur le TP : un fichier
. typage du petit langage fonctionnel
. définition du système de types
. propriétés : progrès, préservation, correction
. interlude : ajout de déclarations locales
   - Section 4.3 des notes de P. Sewell -- vous pouvez ignorer ce qui concerne le typage (relation notée |- )
   - Les parties correspondantes du cours à UPenn, ici, et ici
11/12 . types simples : inférence de types
. FUN annoté
. polymorphisme, début
   - Annotations de types : la partie correspondante du cours à UPenn
   - Sur l'inférence, les parties 5.1 et 5.2 des notes de cours de D. Rémy
   - Sur les métaphores animalières, les alligators (non typés)

Liens, ouvrages de référence

- Ouvrage de référence pour la première partie du cours: Glynn Winskel, The Formal Semantics of Programming Languages, MIT Press (disponible à la bibliothèque).
- Ouvrage de référence pour la deuxième partie du cours: F. Baader et T. Nipkow, Term Rewriting and All That, Cambridge University Press (disponible à la bibliothèque).
- Cours disponibles en ligne:
    . UPenn
    . Cambridge (cliquer sur "Course materials")
    . Harvard
- Sur Coq:
    . tutoriel de Coq
    . Coq in a Hurry, de Y. Bertot
    . une cheatsheet
- Les volumes 1 et 2 de Software foundations (utilisés à UPenn).
- Pour approfondir Knaster-Tarski, B.A. Davey, H.A. Priestley, Introduction to Lattices and Order, Cambridge University Press (disponible à la bibliothèque).

Pour aller plus loin : si le sujet du cours vous plaît, suivez le cours de Xavier Leroy au Collège de France