Course presentation.
Week 1.
Lecture 1 (12/02/2025):
- Introduction.
- Simple types and their set-theoretic semantics.
- Hindley-Longo axioms of λ-models.
- Properties of λ-models.
- The term model.
Lecture 2 (14/02/2025):
- The term model is a λ-model.
- Engeler’s model (two definitions, set-theoretic and type-theoretic).
- Engeler’s model is a λ-model.
Homeworks:
- Prove that the interpration in a λ-model is invariant by β-reduction, i.e.
if t -> u, then ⟦t⟧ = ⟦u⟧.
- Prove the equivalence between the two definitions we gave for the interpretation
in Engeler’s model.
Bibliography:
- Models of the λ-calculus. Hindley and Seldin, Lambda-calculus and combinators: an introduction (Chapter 15).
- If you want some more category theory: Manzonetto’s PhD Thesis (Chapter 1).
Week 2.
Lecture 3 (19/02/2025):
- Typability of head normal forms.
- Completeness of intersection types w.r.t. head termination.
- Soundness of intersection types w.r.t. head termination (via reducibility).
Lecture 4 (21/02/2025):
- Soundness of intersection types w.r.t. head termination (via reducibility), continued.
- Discussion about λ-models and λ-theories.
- Non-idempotent intersection types.
- Soundness and completeness of multi types w.r.t. weak head reduction.
Homeworks:
- Prove that head normal forms are typable, formally.
- Prove that HN(tu) implies HN(t).
- Do multi/intersection types satisfy subject reduction/expansion w.r.t. to the η-law? Remember that t =_η λx.tx when x is not free in t.
Bibliography: