## EXAM: Thursday Jan. 25th, 8:00-11:00, room 103 (first floor, south side)

# 2nd part

## Lecture 11 (Jan. 9th)

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.

Intuitionistic sequents A_{1},...,A_{n} ⊢ B. Left and right rules (⍟L) and (⍟R). Derivable rule.

**Homework 6**: due on January 16th.

## Lecture 12 (Jan. 11th)

Sequent calculus `IL`

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

Monoidal categories (MC). Definition and basic properties. Mac Lane's coherence theorem (admitted).

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

in monoidal categories. Image of ⟦_⟧.

## Lecture 13 (Jan. 16th)

Admissible rule (≠ derivable). Cut elimination of `IL`

. Sub-formula property.

Commutation: exchange rule. Symmetric monoidal categories (SMC).

**Homework 7**: due on January 23th.

## Lecture 14 (Jan. 18th)

Structural rules: contraction and weakening. Internal monoids and comonoids. Comonoid morphisms. Categories of comonoids are cartesian.

Implication. Symmetric monoidal closed categories (SMCC). Intuitionistic Multiplicative Linear Logic (`IMLL`

).

Products and coproducts. Additive connectives &, ⊕, ⊤ and 0. Distributivity of ⊗ over ⊕. Intuitionistic Multiplicative Additive Linear Logic (`IMALL`

).

## Lecture 15 (Jan. 23rd)

Some provable properties in `IMALL`

. Cut elimination for additives.

Modalities. Modal logic `IK`

. Monoidal functors and monoidal natural transformations. Modal logic `IS4`

. Monoidal comonad.

Structural rules restricted to `!A`

as comonoid structures.

Categorical models of `ILL`

. Girard's translation vs coKleisli construction.

## References