Theory Presentation Combinators
Jacques Carette, Russell O'Connor

TL;DR
This paper introduces theory presentation combinators as foundational tools for building scalable libraries of theories, utilizing category theory concepts like contexts and fibered categories.
Contribution
It provides a formal semantics for theory presentation combinators, establishing a theoretical foundation for modular theory development.
Findings
Defines semantics for theory presentation combinators
Uses category theory to model theory composition
Lays groundwork for scalable theory libraries
Abstract
We motivate and give semantics to theory presentation combinators as the foundational building blocks for a scalable library of theories. The key observation is that the category of contexts and fibered categories are the ideal theoretical tools for this purpose.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
