Category theory for computer scientists (2023-2024) - CR15

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 A1,...,An ⊢ 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 A1,...,An ⊢ 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.