### Proofs and Programs Course, LMFI M2, Academic Year 2023-2024

#### Current version of the lecture notes.

Here (13/03/2024).

## Week 1.

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

## Week 2.

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

## Week 3.

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

## Week 4.

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

## Week 5.

##### 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:

##### Bibliography:

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

## Week 6.

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

If you need other references, please email me!

## Old Things.

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