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

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:

• 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 (25/02/2025):

• Quantitative soundness of multi types.
• The complexity of beta-reduction.
• Krivine Abstract Machine

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 6 (05/03/2025):

• KAM invariants.
• Correctness of the KAM, via types.
• Complexity of the KAM, via types.

Lecture 7 (07/03/2025):

• The linear time KAM.
• Correctness and complexity of the linear time KAM.
• How to type the linear time KAM.
• Introduction to the GoI.

Homeworks (due March 14):

• State and prove the depth invariant for the KAM.
• State and prove the environment length invariant for the KAM.
• State and prove the splitting lemma for KAM environments.
• Prove the variable case for the soundness of the KAM.

Lecture 8 (12/03/2025):

• The linear λ-calculus.
• The linear type IAM.
• The linear IAM.
• Easy invariants.

Lecture 9 (14/03/2025):

• The full IAM.
• More easy invariants.
• The exhaustible state invariant.

Homeworks (due March 21 if possible):

• Prove the exhaustible state invariant. HW Sheet.

Bibliography:

• Notes on the IAM.

Lecture 10 (21/03/2025):

• Relationship between the IAM and the SIAM.
• Complexity of the IAM.

Bibliography:

• To be posted.

Lecture 11 (26/03/2025):

• Guest lecture by Rémy Cerda on continuity and Taylor expansion. Notes

Lecture 12 (28/03/2025):

• Imperative programs and their operational semantics.
• Hoare logic.
• Soundness and completeness.

Homeworks (due April 6, strict):

• Can we use Hoare logic to measure the runtime complexity of a program? Consider the following program C: k := 0; while (i>0) do {k := k+1; i := i-1 }. Then prove through Hoare logic that {i>=0}C{k = i}.

Bibliography:

• Dezani, Giovanetti, de’Liguoro, Intersection types, λ-models Link.
• Rémy Cerda’s Thesis Link.
• Hoare logic (and much more): Winskel’s book.