Thèmes : Logique & Preuve, Sémantique –
Cursus : ENS-Cachan - L3 , ENS-Ulm - L3 Jean Goubault-Larrecq Etienne Lozes - TD1 : Alpha conversion, beta réduction, stratégies perpétuelles, systèmes confluent.
- TD2 : Preuve de la confluence du lambda-calcul par les réductions parallèles. Codage des entiers de Church, des listes, et des points fixes.
- TD3 : Théorème de standardisation. Logique combinatoire.
- TD3 : Corrigé.
- TD4 : Modèles de Engeler et de Scott, ou parallèle.
- TD4 : Corrigé.
- TD5 : Typage, correspondance de Curry-Howard.
- TD6 : Normalisation forte, cohérence de la logique propositionnelle classique, incohérence de Russel.
- TD7 : Système F, types de données.