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.

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



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