2026-08-10T16:18:05Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23638 2025-10-27T10:30:31Z ddc:004 open_access

∞-Categorical Models of Linear Logic Harington, Eliès Mimram, Samuel linear logic linear-non-linear adjunction ∞-category spectrum The notion of categorical model of linear logic is now well studied and established around the notion of linear-non-linear adjunction, which encompasses the earlier notions of Seely categories, Lafont categories and linear categories. These categorical structures have counterparts in the realm of ∞-categories, which can thus be thought of as weak forms of models of linear logic. The goal of this article is to formally introduce them and study their relationships. We show that ∞-linear-non-linear adjunctions still play the role of a unifying notion of model in this setting. Moreover, we provide a sufficient condition for a symmetric monoidal ∞-category to be Lafont. Finally, we illustrate our constructions by providing models: we construct linear-non-linear adjunctions that generalize well-known models in relations (and variants based on profunctors or spans), domains and vector spaces. In particular, we introduce a model based on spectra, a homotopical variant of abelian groups. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Eliès Harington and Samuel Mimram 2025 Is Part Of LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2025.23 urn:nbn:de:0030-drops-236381 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.23 eng https://creativecommons.org/licenses/by/4.0/legalcode