• Login

en fr

Cours : LAmbda-calcul et Logique (S2)

Objectifs : Le but de ce cours est de comprendre les bases du lambda-calcul, un formalisme qui est à la fois le cœur des langages de programmation fonctionnels et le langage des preuves dans diverses logiques, intuitionnistes ou classiques, propositionnelles ou non. La correspondance entre langages de programmation et preuves est la correspondance de Curry-Howard. Ce cours se déroule en trois parties: (1) le lambda-calcul pur, ses propriétés, y compris le fait qu'il code exactement les fonctions calculables; (2) logique et démonstrations, la correspondance de Curry-Howard; (3) implémentations, machines, et lambda-calculs à substitutions explicites.

Plan détaillé :

1. Réduction, (non-)terminaison, notions de confluence.
2. Théorème des développements finis, confluence.
3. Pouvoir expressif: on peut exprimer toutes les fonctions récursives en lambda-calcul.
4. Stratégies de réduction, standardisation.
5. Modèles du lambda-calcul pur.
6. Le lambda-calcul simplement typé. Correspondance de Curry-Howard. La logique propositionnelle intuitionniste minimale.
7. Autres logiques propositionnelles.
8. Logique classique propositionnelle.
9. Logique et arithmétique du premier ordre.
10. Système F, logique et arithmétique du second ordre.
11. Machines, lambda-calculs à substitutions explicites.

Références :

• Notes de cours, lien "Logic and Computer Science---the Lambda-Calculus"
• Henk Barendregt. The Lambda Calculus, Its Syntax and Semantics. T. 103. Studies in Logic and the Foundations of Mathematics. Amsterdam : North-Holland Publishing Company, 1984.
• Jean-Louis Krivine. Lambda-calcul, types et modèles. Masson, 1992.
• Jean-Yves Girard, Yves Lafont et Paul Taylor. Proofs and Types. T. 7. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989.