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.
J’utiliserai des transparents détaillés, que voici:
- Introduction, réduction, (non-)terminaison, notions de confluence. La vidéo, et la version courte (sans les différentes étapes d’animation) des transparents.
- Théorème des développements finis, confluence. La vidéo, et la version courte des transparents.
- 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.
- 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.
- 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.
- Lambda-calcul simplement typé. La vidéo. La version courte des transparents.
- Autres logiques propositionnelles. La vidéo. La version courte des transparents.
- Logique classique propositionnelle. La vidéo. La version courte des transparents.
- Logique et arithmétique du premier ordre. La vidéo. La version courte des transparents.
- 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.
- 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.
- 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.
- 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. Voici celui de 2024, et un corrigé. Il était à rendre pour le mardi 26 mars 2024, par email. Voici le patron de réponse, et le fichier prooftree.sty, pour écrire des dérivations.
Voici le sujet de l’examen 2024, et un corrigé.
La note finale sera max(examen, (examen+partiel)/2). L’examen a eu lieu le mardi 28 mai 2024.