Categorical models of Linear Logic with fixed points of formulas
Thomas Ehrhard, Farzad Jafarrahmani
Abstract
We develop a categorical semantics of μLL, a version of propositional Linear Logic with least and greatest fixed points extending David Baelde's propositional μMALL with exponentials. Our general categorical setting is based on Seely categories and on strong functors acting on them. We exhibit two simple instances of this setting. In the first one, which is based on the category of sets and relations, least and greatest fixed points are interpreted in the same way. In the second one, based on a category of sets equipped with a notion of totality (non-uniform totality spaces) and relations preserving it, least and greatest fixed points have distinct interpretations. This latter model shows that μLL enjoys a denotational form of normalization of proofs.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext 2105cdc9-47d6-4b27-8aa0-e8ac1764ead5Cited by top-tier papers1
Ask how each one uses itRelated papers
- On the denotation of circular and non-wellfounded proofs in linear logic with fixed pointsThomas Ehrhard, Farzad Jafarrahmani, Alexis SaurinLICS 2025
- A Constructive Logic with Classical Proofs and RefutationsPablo Barenbaum, Teodoro FreundLICS 2021
- Taylor Expansion as a Monad in Models of DiLLMarie Kerjean, Jean-Simon Pacaud LemayLICS 2023 · 5 citations
- Interpreting De Finetti's Theorem in the Category of Integrable ConesRaphaëlle CrubilléLICS 2026
- Linear-Algebraic Models of Linear Logic as Categories of Modules over Σ-Semirings✱Takeshi Tsukada, Kazuyuki AsadaLICS 2022 · 4 citations
