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.

Homework (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).

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.

Homework (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.

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

Homework (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.

Lecture 7-8:

• KAM complexity analysis.
• Typing the KAM with non-idempotent intersection types.
• Making the KAM linear and corresponding types.
• The problem of space complexity.

Homework (due 25/03/2026):

• Prove the splitting lemma for the KAM types, as it is needed in the proof of subject reduction.
• Provide the two definitions of decoding, environments first and stack first, and prove that they are equivalent.

Bibliography:

• Space complexity: an historical paper, and the state of the art paper 1 paper 2.

Lecture 9-10:

• The linear λ-calculus.
• The !-calculus and Girard’s translations.
• Introduction to proof-nets and the encoding of the λ-calculus in linear logic.
• The geometry of interaction.

Bibliography:

• Geometry of interaction: notes
• Bang-calculus: paper
• Linear types: paper

Lecture 11-12:

• Curry-Howard correspondence and intersection types.
• Imperative programming: operational semantics.
• Hoare logic and its soundness.

Homework (due 26/04/2026):

• Prove soundness for Hoare logic formally: the while case.
• Consider the program x := n; while (x > 1) do x := x * (x - 1). We have already seen in class the case n = 2. Study the program behavior for the other non-negative values of n, formally (the cases n = 0 and n = 1 is very simple, the cases n > 2 require some more effort).

Bibliography:

• The polyadic λ-calculus paper
• Hoare logic (and much more): Winskel’s book