## EXAMEN: jeudi 14 novembre (durée 3h) en salle B1

#### Début, au choix de chaque étudiant.e, soit à 13h (fin à 16h) soit à 13h30 (fin à 16h30) : merci de nous informer par mail de votre choix au plus tôt.

# 2nd part

## Lecture 11 (Oct. 17th)

Introduction: Curry-Howard-Lambek correspondence. What would be a category of proofs? Core sequent calculus `L`

: sequents A ⊢ B, rules (*ax*) and (*cut*). Intepretation ⟦_⟧ of `L`

in a category. Kernel and image of ⟦_⟧. Cut reduction.

Adding a (endo)functor. Unary connective □ (modality), rule (□), categorical interpretation, cut reduction, axiom reduction.

Adding a (endo)bifunctor. Binary connective ⍟, rule (⍟), categorical interpretation, cut reduction, axiom reduction.
Units.

Sequent calculus `IL`

: intuitionistic sequents A_{1},...,A_{n} ⊢ B, left and right rules (⍟L) and (⍟R).

**Homework 5**: due on October 24th.

## Lecture 12 (Oct. 21st)

Monoidal categories (MC). Definition and basic properties. Mac Lane's coherence theorem (admitted, proof of λ₁ = ρ₁).

Left and right rules (1L) and (1R). Categorical interpretation ⟦_⟧ of `IL`

in monoidal categories.

Derivable and admissible rules. Axiom expansion.

## Lecture 13 (Oct. 24th)

Invariance of ⟦_⟧ under axiom expansion. Image of ⟦_⟧. Cartesian categories are monoidal.

Cut elimination for `IL`

. Sub-formula property.

Commutation: exchange rule. Symmetric monoidal categories (SMC). Cut elimination. Cartesian categories are symmetric monoidal.

**Homework 6 (corrected version for exercise 2)**: due on November 7th.

## Lecture 14 (Nov. 4th)

## Lecture 15 (Nov. 7th)

## Exam (Nov. 14th)

## References