Document Open Access Logo

∞-Categorical Models of Linear Logic

Authors Eliès Harington , Samuel Mimram

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2025.23.pdf
  • Filesize: 1.53 MB
  • 20 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Linear logic
Keywords
  • linear logic
  • linear-non-linear adjunction
  • ∞-category
  • spectrum

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

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.

Cite As Get BibTex

Eliès Harington and Samuel Mimram. ∞-Categorical Models of Linear Logic. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 23:1-23:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.FSCD.2025.23

Author Details

Eliès Harington
  • LIX, CNRS, École polytechnique, Institut Polytechnique de Paris, 91120 Palaiseau, France
Samuel Mimram
  • LIX, CNRS, École polytechnique, Institut Polytechnique de Paris, 91120 Palaiseau, France

References

  1. Samson Abramsky and Achim Jung. Handbook of Logic in Computer Science, volume 3, chapter Domain theory, pages 1-168. Clarendon Press, Oxford, 1994. Google Scholar
  2. Jiří Adámek and Jiří Rosickỳ. Locally presentable and accessible categories, volume 189. Cambridge University Press, 1994. Google Scholar
  3. Gregory Arone and Michael Ching. Goodwillie calculus. In Handbook of homotopy theory, pages 1-38. Chapman and Hall/CRC, 2020. Google Scholar
  4. Michael Barr. Coalgebras over a commutative ring. Journal of Algebra, 32(3):600-610, 1974. Google Scholar
  5. Michael Barr. *-autonomous categories and linear logic. Mathematical Structures in Computer Science, 1(2):159-178, 1991. URL: https://doi.org/10.1017/S0960129500001274.
  6. Jon Beck. Distributive laws. In Seminar on Triples and Categorical Homology Theory, pages 119-140, Berlin, Heidelberg, 1969. Springer Berlin Heidelberg. Google Scholar
  7. Nick Benton. A mixed linear and non-linear logic: Proofs, terms and models. In International Workshop on Computer Science Logic, pages 121-135. Springer, 1994. Google Scholar
  8. John D. Berman. Higher lawvere theories. Journal of Pure and Applied Algebra, 224(9):106362, 2020. Google Scholar
  9. Gavin M. Bierman. What is a categorical model of intuitionistic linear logic? In Typed Lambda Calculi and Applications, Second International Conference on Typed Lambda Calculi and Applications, TLCA, volume 902 of Lecture Notes in Computer Science, pages 78-93. Springer, 1995. URL: https://doi.org/10.1007/BFB0014046.
  10. Pierre-Louis Curien. Operads, clones, and distributive laws. In Operads and universal algebra, pages 25-49. World Scientific, 2012. Google Scholar
  11. Valeria de Paiva. Categorical Semantics of Linear Logic for All, pages 181-192. Springer Netherlands, Dordrecht, 2014. Google Scholar
  12. Sanath Devalapurkar and Peter Haine. On the James and Hilton-Milnor splittings, and the metastable EHP sequence. Documenta Mathematica, 26:1423-1464, 2021. Google Scholar
  13. Eric Finster, Samuel Mimram, Maxime Lucas, and Thomas Seiller. A cartesian bicategory of polynomial functors in homotopy type theory. In Proceedings 37th Conference on Mathematical Foundations of Programming Semantics, MFPS 2021, volume 351 of EPTCS, pages 67-83, 2021. URL: https://doi.org/10.4204/EPTCS.351.5.
  14. Marcelo Fiore, Zeinab Galal, and Hugo Paquet. Stabilized profunctors and stable species of structures. Logical Methods in Computer Science, 20, 2024. URL: https://doi.org/10.46298/LMCS-20(1:17)2024.
  15. Marcelo Fiore, Nicola Gambino, and Martin Hyland. Monoidal bicategories, differential linear logic, and analytic functors. Preprint, 2024. URL: https://arxiv.org/abs/2405.05774.
  16. Marcelo Fiore, Nicola Gambino, Martin Hyland, and Glynn Winskel. The cartesian closed bicategory of generalised species of structures. Journal of the London Mathematical Society, 77(1):203-220, 2008. Google Scholar
  17. Grant A. Fraser. The semilattice tensor product of distributive lattices. Transactions of the American Mathematical Society, 217:183-194, 1976. Google Scholar
  18. Nicola Gambino and Joachim Kock. Polynomial functors and polynomial monads. Mathematical proceedings of the cambridge philosophical society, 154(1):153-192, 2013. Google Scholar
  19. David Gepner, Rune Haugseng, and Joachim Kock. ∞-operads as analytic monads. International Mathematics Research Notices, 2022(16):12516-12624, 2022. Google Scholar
  20. Jean-Yves Girard. Linear logic. Theoretical computer science, 50(1):1-101, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  21. Jean-Yves Girard. Normal functors, power series and λ-calculus. Annals of pure and applied logic, 37(2):129-177, 1988. URL: https://doi.org/10.1016/0168-0072(88)90025-5.
  22. Thomas G Goodwillie. Calculus III: Taylor series. Geometry & Topology, 7(2):645-711, 2003. Google Scholar
  23. Elies Harington and Samuel Mimram. Polynomials in homotopy type theory as a Kleisli category. In Proceedings of MFPS XL, volume 4 of Electronic Notes in Theoretical Informatics and Computer Science, 2024. Google Scholar
  24. Rune Haugseng. On (co) ends in ∞-categories. Journal of Pure and Applied Algebra, 226(2):106819, 2022. Google Scholar
  25. Simon Henry and Nicholas J. Meadows. Higher theories and monads. Preprint, 2021. URL: https://arxiv.org/abs/2106.02706.
  26. Martin Hyland and Andrea Schalk. Abstract games for linear logic extended abstract. Electronic Notes in Theoretical Computer Science, 29:127-150, 1999. Google Scholar
  27. Martin Hyland and Andrea Schalk. Glueing and orthogonality for models of linear logic. Theoretical computer science, 294(1-2):183-231, 2003. URL: https://doi.org/10.1016/S0304-3975(01)00241-9.
  28. Bart Jacobs. Semantics of weakening and contraction. Annals of Pure and Applied Logic, 69(1):73-106, 1994. URL: https://doi.org/10.1016/0168-0072(94)90020-5.
  29. André Joyal. Quasi-categories and Kan complexes. Journal of Pure and Applied Algebra, 175(1-3):207-222, 2002. Google Scholar
  30. William F. Keigher. Symmetric monoidal closed categories generated by commutative adjoint monads. Cahiers de topologie et géométrie différentielle, 19(3):269-293, 1978. Google Scholar
  31. Marie Kerjean. Weak topologies for linear logic. Logical Methods in Computer Science, 12, 2016. URL: https://doi.org/10.2168/LMCS-12(1:3)2016.
  32. Joachim Kock. Data types with symmetries and polynomial functors over groupoids. Electronic Notes in Theoretical Computer Science, 286:351-365, 2012. Google Scholar
  33. Joachim Kock, André Joyal, Michael Batanin, and Jean-François Mascari. Polynomial functors and opetopes. Advances in Mathematics, 224(6):2690-2737, 2010. Google Scholar
  34. Yves Lafont. Logiques, catégories et machines. PhD thesis, Université Paris 7, 1988. Google Scholar
  35. Jacob Lurie. Higher topos theory. Princeton University Press, 2009. Google Scholar
  36. Jacob Lurie. Higher algebra. Preprint, 2017. URL: https://people.math.harvard.edu/~lurie/papers/HA.pdf.
  37. Jacob Lurie. Kerodon. https://kerodon.net, 2018.
  38. Paul-André Mellies. Categorical semantics of linear logic. Panoramas et syntheses, 27:15-215, 2009. Google Scholar
  39. Paul-André Melliès and Nicolas Tabareau. Resource modalities in tensor logic. Annals of Pure and Applied Logic, 161(5):632-653, 2010. URL: https://doi.org/10.1016/J.APAL.2009.07.018.
  40. Paul-André Melliès, Nicolas Tabareau, and Christine Tasson. An explicit formula for the free exponential modality of linear logic. Mathematical Structures in Computer Science, 28(7):1253-1286, 2018. URL: https://doi.org/10.1017/S0960129516000426.
  41. Paul-André Melliès. Categorical models of linear logic revisited. Unpublished manuscript, 2003. URL: https://hal.science/hal-00154229.
  42. nLab authors. commutative algebraic theory. https://ncatlab.org/nlab/show/commutative+algebraic+theory, February 2025. URL: https://ncatlab.org/nlab/revision/commutative+algebraic+theory/39.
  43. nLab authors. Goodwillie calculus. https://ncatlab.org/nlab/show/Goodwillie+calculus#GoodwillieDerivativeOfExponentialModality, February 2025. URL: https://ncatlab.org/nlab/show/Goodwillie+calculus#GoodwillieDerivativeOfExponentialModality/68.
  44. Emily Riehl. Categorical homotopy theory, volume 24. Cambridge University Press, 2014. Google Scholar
  45. R. A. G. Seely. Linear logic, ∗-autonomous categories and cofree coalgebras. In Categories in computer science and logic, Contemp. Math., pages 371-382. American Mathematical Society, 1989. Google Scholar
  46. Moss E. Sweedler. Hopf algebras, volume 44 of Mathematics lecture note series. W. A. Benjamin, 1969. Google Scholar
  47. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  48. Benoît Valiron and Steve Zdancewic. Modeling simply-typed lambda calculi in the category of finite vector spaces. Scientific Annals of Computer Science, 24(2), 2014. URL: https://doi.org/10.7561/SACS.2014.2.325.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact