MPRI: Logique linéaire et paradigmes de calcul - 2023/2024


gmanzone[at]irif dot fr

Part 3 - Lambda Calculus, Type Systems and Models

These lectures are part of a larger cours of Linear logic and logical paradigms of calculus.
Each lecture is 3 hours long, and it is composed by 2 hours of CM, and 1 hour of TD.

Salle de cours / Horaire

Salle 1002, premier étage, Bát Sophie Germain, Univ. de Paris Cité.
Le mardi de 16h15 à 19h15.

Contrôle: 5 mars 2024

Documents autorisés: The inference rules of the type systems will be given as an appendix.

Slides:

1) 5 December 2023 Simply Typed Lambda Calculus. Properties, WN, 3 proofs of SN.
2) 12 December 2023 Intersection types, Turing-equivalence between DP in simply typed and IHP in CDV.
3) 9 January 2024 Böhm tree semantics, Filter Models and Approximation Theorems
4) 16 January 2024 Multi-types, Approximation Theorem, exact bounds.

Sujets de TD:

1) Simply Typed Lambda Calculus. Multiset ordering and well-foundedness.
2) Intersection type systems. Saturated sets - the revenge.
3) Böhm trees and filter models.
4) Multi-types and approximations. In addition: Lecture notes by Beniamino Accattoli

Bibliographie

Dernière mise à jour: 23 janvier 2024