Lecture 1 (27/02/2024):

• Introduction.
• Review of the lambda-calculus (beta-reduction, head reduction, head normal forms).
• Simple types and their set-theoretic semantics.
• The strict intersection type system.
• Subject reduction.
• Subject expansion.

Lecture 2 (28/02/2024):

• Typability of head normal forms.
• Completeness of intersection types w.r.t. termination.
• Soundness of intersection types w.r.t. termination (via reducibility).

Homeworks:

• Read Chapters Naturals and Induction.
• Exercise *-distrib-+ (PLFA - Induction), with and without rewrite.
• Prove formally the lambda-abstraction case (correctly handling all the substitutions) of the fundamental lemma.
• Optional. Prove that: HN(tu) implies HN(t).
• Optional. Exercise +*^ (PLFA - Induction).

Bibliography:

• Set theoretic semantics: Fiore’s slides (Ignore everything which is not the simply typed lambda-calculus e.g. fixed points and if-then-else).
• 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 3 (05/03/2024):

• Hindley-Longo axioms of λ-models.
• The term model.
• Properties of λ-models.
• Engeler’s model (definition).

Lecture 4 (06/03/2024):

• Engeler’s model is a λ-model.
• Non-idempotent intersection types.
• Completeness of multi types w.r.t. head reduction.

Homeworks:

• Read Chapter Relations.
• Exercise <-trans (PLFA - Relation).
• Prove that both the term model and Engeler’s model satisfy axiom 5.
• Optional. Exercise o+o≡e (PLFA - Relation).

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 5 (12/03/2024):

• Soundness of multi types w.r.t. head reduction.
• Multi types for weak head reduction and closed terms.
• Quantitative characterization theorem (statement only).
• Reasonable models and the size explosion problem.

Lecture 6 (13/03/2024):

• Krivine’s Abstract Machine: its correctness and complexity.
• The KAM and multi types in Agda (first part): Bob Atkey’s code.

Homeworks:

• Prove the quantitative characterization theorem: ⊢^n t:★ iff t->^n_{wh} λx.u. Consider t closed, this will simplify a lot the substitution lemma, and consider the subject expansion for granted. ⊢^n t:A means that t is typed with A using a type derivation containing exaclty n abstraction (not abstraction-★) rules. For those who were not in class: the type system is the one in Beniamino’s notes for head reduction + the axiom ⊢ λx.t:★. ★ is the only base type.

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 (19/03/2024):

• The KAM and multi types in Agda (second part): Bob Atkey’s code.
• The optimized KAM and its correctness.

Lecture 8 (20/03/2024):

• The complexity of the optimized KAM.
• Multi types and the optimized KAM.
• λ-theories: sensibility, consistency, =ᵦ, 𝓗, 𝓗*, solvability.

Homeworks:

• Prove that =ᵦ ⊆ 𝓗*.
• Do multi types satisfy subject reduction/expansion w.r.t. to the η-law? Remember that t =_η λx.tx when x is not free in t.

Bibliography:

• λ-theories: Beniamino Accattoli’s slides.

Lecture 9 (26/03/2024):

• Genericity lemma, and sensibility of 𝓗*.
• 𝓗* is the maximal consistent and sensible λ-theory.

Lecture 10 (27/03/2024):

• Böhm trees, and their order.
• Syntactic approximation theorem (sketch).
• Semantic approximation theorem.
• Barendregt’s Kite of λ-theories.

Homeworks:

• Homework

Bibliography:

• λ-theories, part 2: Giulio Manzonetto’s slides.

Lecture 11 (02/04/2024):

• Inhabitation in non-idempotent intersection types (by Victor Arrial)

Lecture 12 (03/04/2024):

• Imperative programs and their operational semantics.
• Hoare logic.
• Soundness (with proof) and completeness (without proof).
• Proving termination.

Bibliography:

• Inhabition: Paper.
• Hoare logic (and much more): Winskel’s book.

Presentation

• We will use Agda during the course. You should have Agda 2.6.4 installed with the agda-stdlib 1.7.3. Beware, the 2.0 version does not work with the book.
• Installation instructions are Here.
• Installing the book: link. You can use the simpler

git clone --depth 1 https://github.com/plfa/plfa.github.io plfa

to avoid cloning the stdlib you have already insalled.