Proofs and Programs: Advanced Tools, Linear Logic and Quantitative Semantics, LMFI M2, Academic Year 2025-2026
Last version of the notes: here (02/02/2026).
Week 1 (14/01/2026).
Lecture 1-2:
- Introduction.
- Recap on the untyped λ-calculus.
- Simple types and their set-theoretic semantics.
- Intensional vs. extensional expressivity of typed λ-calculi.
- Hindley-Longo axioms of λ-models.
- Properties of λ-models.
- The term model.
- The term model is a λ-model.
Homeworks (due 10/02/2026):
- Is the set-theoretic model also invariant for η-equivalence? Prove or disprove it.
- Prove that the term model satisfies point 5 of the definition of λ-model.
- Modify the definition of λ-model so that also η-equality is derivable and prove it.
- Does the term model satisfy this new definition?
Bibliography:
- Models of the λ-calculus. Hindley and Seldin, Lambda-calculus and combinators: an introduction (Chapter 15).
Week 2 (11/02/2026).
Lecture 3-4:
- Engeler’s model.
- Type-theoretic presentation (intersection types).
- Typability of normal forms.
- Subject expansion.
- Completeness.
- Soundness by reducibility.
- The Engeler’s model is a lambda-model.
Homeworks (due 04/03/2026):
- Prove the case H = λx.H’ of subject expansion.
- Prove that the set theoretic and the type theoretic definition’s of Engeler’s model are equivalent.
- Prove that HN(tu) implies HN(t).
- Prove that Engeler’s model satisfies axioms 3 and 5 of λ-model (HINT: use the presentation which is more handy for this proof).
- Prove subject reduction for intersection types (HINT: there’s an easy non-syntactical way)
- Does Engeler’s model satisfy η-equivalence?
Bibliography:
- Models of the λ-calculus. Hindley and Seldin, Lambda-calculus and combinators: an introduction (Chapter 16F).
- If you want some more category theory: Manzonetto’s PhD Thesis (Chapter 1).
- Strict intersection types: van Bakel’s survey.
- A tutorial on logical relations: OPLSS notes.
- A survey on intersection types: Dezani and Bono’s survey.
Week 3 (04/03/2026).
Lecture 5-6:
- Discussion about λ-models and λ-theories.
- Non-idempotent intersection types.
- Soundness and completeness of multi types w.r.t. weak head reduction.
- The complexity of beta-reduction.
- Krivine’s Abstract Machine
Homeworks (due 18/03/2026):
- Prove the invariant that relates the number of ‘sea’ and ‘beta’ transitions in a KAM run.
- Prove that length of the environment of reachable states is limited is limited by the size of the original term under evaluation.
- What is instead the maximum ‘depth’ of environments of reachable states?
Bibliography:
- Multi types: Beniamino Accattoli’s notes.
- Reasonable cost models: Beniamino Accattoli’s notes.
- Abstract machines: Beniamino Accattoli’s notes and these papers 1 and 2.