Linear Hyperdoctrines and Comodules
Mariana Haim, Octavio Malherbe
TL;DR
This paper introduces linear hyperdoctrines constructed from categories of comodules indexed by coalgebras, providing a categorical framework to model first-order linear logic.
Contribution
It presents new examples of linear hyperdoctrines based on comodules, expanding the categorical models available for linear logic.
Findings
Examples of linear hyperdoctrines from comodules
Framework for modeling first-order linear logic
Connections between coalgebras and logical structures
Abstract
In this exposition, we get examples of what is called a "linear hyperdoctrine", based on categories of comodules indexed by coalgebras. This structures can model first order linear logic.
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.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Pharmacological Receptor Mechanisms and Effects