Cours de L3 "Logique et informatique – lambda-calcul"

Le programme, en trois polys:

• Lambda-calcul pur, (non-)terminaison, confluence, standardisation. Version en gros caractères.
• 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). Version en gros caractères.
• Machines, lambda-calculs à substitutions explicites, et propriétés mathématiques d'iceux. Version en gros caractères.

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 (HA₂), 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

Le partiel, sous forme d'un devoir à la maison (et ici en plus grand), à rendre le 13 avril 2026 (le 18 avril en cas de tiers-temps supplémentaire) au plus tard en pdf par email. Voici le patron de réponse. (Deux fichiers, dm2026-copie.tex et prooftree.sty. Commentez \bigfalse et décommentez \bigtrue pour une version en grand.)

En voici un corrigé, et le même en plus grand.

Voici le sujet de l'examen 2026 (et ici en gros caractères), et un corrigé (et ici en gros caractères).

La note finale sera max(examen, (examen+partiel)/2). L'examen a traditionnellement lieu la dernière semaine de mai.