Displayed Monoidal Categories for the Semantics of Linear Logic
summary
Formalized a reusable library of monoidal-category constructions in UniMath using new displayed monoidal categories that let complicated monoidal structures be built in layers instead of monolithic definitions. The work constructs linear–nonlinear models (including Lafont categories and linear categories) inside Coq, removes duplicated code, and scales better during proof checking, producing fully machine-checked models of the bang modality and the comonad-based tensor that are usable in further formalizations.
AI-written summary · about
chapters (15)
- 0:00Introduction
- 0:48What is category theory
- 2:11Category theory in logic
- 4:40Monoidal categories overview
- 7:53Monoidal categories in semantics
- 9:20Models of linear logic
- 11:09Linear logic features
- 13:15Linear-nonlinear models
- 15:22Lafont’s coronoid model
- 16:25Challenges in constructing monoidal categories
- 18:11Modular group construction
- 19:35Displayed structures
- 21:43Displayed monoidal categories
- 23:07Conclusion and takeaways
- 23:51Q&A
related talks
23mFormalizing Monoidal Categories and Actions for Syntax with Binders
42mEvaluating Linear Functions to Symmetric Monoidal Categories
23mImplementing a category-theoretic framework for typed abstract syntax
26m2-Functoriality of Initial Semantics, and Applications
20mFully Abstract Models for Effectful λ-Calculi via Category-Theoretic Logica
27mFunctorial Semantics for Partial Theories
56mCalculating Intuitionistic Logic in Scala
29mMechanized monadic equational reasoning for ML references