Categorical models of Linear Logic with fixed points of formulas
Thomas Ehrhard, Farzad Jafarrahmani
摘要
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.
问问这篇 Paper
智能体会读完全文。
Lune 把这篇 Paper 索引到了每一个公式,引用它的顶会 Paper 也一样。你提问,回答直接引用原文。
引用它的顶会 Paper1
问问它们各自怎么用它相关 Paper
- 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 次
- 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 次
