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.
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 ⟦_⟧.
Admissible rule (≠ derivable). Cut elimination of IL. Sub-formula property.
Commutation: exchange rule. Symmetric monoidal categories (SMC).
Homework 7: due on January 23th.
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).
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.