Cours de L3 “Logique et informatique – lambda-calcul”

Le programme, en trois polys:

  • Lambda-calcul pur, (non-)terminaison, confluence, standardisation.
  • Lambda-calcul typé, correspondances de Curry-Howard pour diverses logiques, classiques ou intuitionnistes, allant de la logique propositionnelle minimale (types simples) à l’arithmétique du second ordre (système F).
  • Machines, lambda-calculs à substitutions explicites, et propriétés mathématiques d’iceux.

Les TDs sont disponibles sur la page de Stéphane Le Roux.

J’utiliserai des transparents détaillés, que voici:

  1. Introduction, réduction, (non-)terminaison, notions de confluence. La vidéo, et la version courte (sans les différentes étapes d’animation) des transparents.
  2. Théorème des développements finis, confluence. La vidéo, et la version courte des transparents.
  3. Pouvoir expressif. La vidéo, dans laquelle, outre les questions de pouvoir expressif, on parle aussi de stratégies de réduction, et on énonce le théorème de standardisation. La version courte des transparents.
  4. Stratégies de réduction, standardisation. La vidéo, dans laquelle nous avons aussi commencé à parler de modèles, jusqu’à introduire la notion de dcpo. La version courte des transparents.
  5. Modèles du lambda-calcul pur. La version courte des transparents. La vidéo. Nous y avons aussi traité des quelques premiers transparents de la séance suivante.
  6. Lambda-calcul simplement typé. La vidéo. La version courte des transparents.
  7. Autres logiques propositionnelles. La vidéo. La version courte des transparents.
  8. Logique classique propositionnelle. La vidéo. La version courte des transparents.
  9. Logique et arithmétique du premier ordre. La vidéo. La version courte des transparents.
  10. Système F, logique et arithmétique du second ordre. La vidéo, qui s’arrête au transparent 121, à la fin de la preuve de normalisation forte du système F. La version courte des transparents.
  11. Machines, lambda-calculs à substitutions explicites, partie 1. La vidéo (4 mai 2021), qui termine la séance précédente (HA2), et va jusqu’au transparent 89, où l’on a introduit la notation de de Bruijn mais on ne l’a pas encore expliquée (par l’exemple; cette explication manque sur la vidéo ainsi que sur la suivante). La version courte des transparents.
  12. Machines, lambda-calculs à substitutions explicites, partie 2. La vidéo du 11 mai 2021, et celle du 18 mai 2021, qui se suivent. La version courte des transparents.
  13. Optionnellement: A-traduction de Friedman et traduction en style de passage à la continuation. Eh non, on ne l’a pas faite, tant pis.

Examen

Il y aura un partiel, à mi-parcours, qui prendra la forme d’un devoir à la maison, que voici. A rendre pour le mardi 12 avril, par email ou en présence. Voici le patron de réponse, et le fichier prooftree.sty, pour écrire des dérivations. Et voici un corrigé possible.

L’examen aura lieu en présentiel le mardi 31 mai 2022, en salle 3E31. Voici le sujet de l’examen 2022, et un corrigé.

La note finale sera max(examen, (examen+partiel)/2).