Formalizing Monoidal Categories and Actions for Syntax with Binders
summary
Mechanization of syntax with binders uses Coq + UniMath to formalize semantic signatures, initial algebras, monad-like substitution and the notion of strength for pointed endofunctors. The claim is that generalizing from concrete functor categories to monoidal categories and then to bicategories removes fragile hidden identity insertions, prevents excessive unfoldings and type-check failures, and makes natural-transformation composition and substitution laws type-check and proofs readable; several lemmas become infeasible without these abstractions.
AI-written summary · about
chapters (10)
- 0:00Intro
- 0:41Overview
- 1:33Formalization setting
- 5:01Problems when formalizing math
- 6:42Study simply typed languages
- 7:51Semantic signatures: Signature functor
- 12:07Issue of composition
- 17:12Benefits of using monoidal categories
- 17:43Abstraction for studying the signature functor
- 20:57Conclusion
related talks
23mImplementing a category-theoretic framework for typed abstract syntax
30mDisplayed Monoidal Categories for the Semantics of Linear Logic
21mFunctorial Syntax for All
28mTowards Light-Weight Operational Reasoning for Languages with Binders, Categorically
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders
26m2-Functoriality of Initial Semantics, and Applications
27mUnivalent Double Categories
25mBinding Syntax for Dependently-Typed Programs