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: