Displayed Monoidal Categories for the Semantics of Linear Logic
Pages 260 - 273
Abstract
We present a formalization of different categorical structures used to interpret linear logic. Our formalization takes place in UniMath, a library of univalent mathematics based on the Coq proof assistant.
All the categorical structures we formalize are based on monoidal categories. As such, one of our contributions is a practical, usable library of formalized results on monoidal categories. Monoidal categories carry a lot of structure, and instances of monoidal categories are often built from complicated mathematical objects. This can cause challenges of scalability, regarding both the vast amount of data to be managed by the user of the library, as well as the time the proof assistant spends on checking code. To enable scalability, and to avoid duplication of computer code in the formalization, we develop "displayed monoidal categories". These gadgets allow for the modular construction of complicated monoidal categories by building them in layers; we demonstrate their use in many examples. Specifically, we define linear-non-linear categories and construct instances of them via Lafont categories and linear categories.
References
[1]
Samson Abramsky and Guy McCusker. 1999. Game Semantics. In Computational Logic, Ulrich Berger and Helmut Schwichtenberg (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 1–55. isbn:978-3-642-58622-4
[2]
Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niccolò Veltri, and Niels van der Weide. 2021. Bicategories in univalent foundations. Math. Struct. Comput. Sci., 31, 10 (2021), 1232–1269. https://doi.org/10.1017/S0960129522000032
[3]
Benedikt Ahrens and Peter LeFanu Lumsdaine. 2019. Displayed Categories. Log. Methods Comput. Sci., 15, 1 (2019), https://doi.org/10.23638/LMCS-15(1:20)2019
[4]
Steve Awodey, Jonas Frey, and Sam Speight. 2018. Impredicative Encodings of (Higher) Inductive Types. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, Anuj Dawar and Erich Grädel (Eds.). ACM, 76–85. https://doi.org/10.1145/3209108.3209130
[5]
Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, and Bas Spitters. 2017. The HoTT library: a formalization of homotopy type theory in Coq. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017, Yves Bertot and Viktor Vafeiadis (Eds.). ACM, 164–172. https://doi.org/10.1145/3018610.3018615
[6]
P. N. Benton. 1994. A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models (Extended Abstract). In Computer Science Logic, 8th International Workshop, CSL ’94, Kazimierz, Poland, September 25-30, 1994, Selected Papers, Leszek Pacholski and Jerzy Tiuryn (Eds.) (Lecture Notes in Computer Science, Vol. 933). Springer, 121–135. https://doi.org/10.1007/BFb0022251
[7]
P. N. Benton, Gavin M. Bierman, Valeria de Paiva, and Martin Hyland. 1992. Linear Lambda-Calculus and Categorial Models Revisited. In Computer Science Logic, 6th Workshop, CSL ’92, San Miniato, Italy, September 28 - October 2, 1992, Selected Papers, Egon Börger, Gerhard Jäger, Hans Kleine Büning, Simone Martini, and Michael M. Richter (Eds.) (Lecture Notes in Computer Science, Vol. 702). Springer, 61–84. https://doi.org/10.1007/3-540-56992-8_6
[8]
P. N. Benton, Gavin M. Bierman, Valeria de Paiva, and Martin Hyland. 1993. A Term Calculus for Intuitionistic Linear Logic. In Typed Lambda Calculi and Applications, International Conference on Typed Lambda Calculi and Applications, TLCA ’93, Utrecht, The Netherlands, March 16-18, 1993, Proceedings, Marc Bezem and Jan Friso Groote (Eds.) (Lecture Notes in Computer Science, Vol. 664). Springer, 75–90. https://doi.org/10.1007/BFb0037099
[9]
Gavin M. Bierman. 1995. 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 ’95, Edinburgh, UK, April 10-12, 1995, Proceedings, Mariangiola Dezani-Ciancaglini and Gordon D. Plotkin (Eds.) (Lecture Notes in Computer Science, Vol. 902). Springer, 78–93. https://doi.org/10.1007/BFb0014046
[10]
Ana C. Calderon and Guy McCusker. 2010. Understanding Game Semantics Through Coherence Spaces. In Proceedings of the 26th Conference on the Mathematical Foundations of Programming Semantics, MFPS 2010, Ottawa, Ontario, Canada, May 6-10, 2010, Michael W. Mislove and Peter Selinger (Eds.) (Electronic Notes in Theoretical Computer Science, Vol. 265). Elsevier, 231–244. https://doi.org/10.1016/j.entcs.2010.08.014
[11]
Alberto Carraro, Thomas Ehrhard, and Antonino Salibra. 2010. Exponentials with Infinite Multiplicities. In Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings, Anuj Dawar and Helmut Veith (Eds.) (Lecture Notes in Computer Science, Vol. 6247). Springer, 170–184. https://doi.org/10.1007/978-3-642-15205-4_16
[12]
Kaustuv Chaudhuri, Leonardo Lima, and Giselle Reis. 2019. Formalized meta-theory of sequent calculi for linear logics. Theor. Comput. Sci., 781 (2019), 24–38. https://doi.org/10.1016/j.tcs.2019.02.023
[13]
Vikraman Choudhury and Marcelo Fiore. 2023. Free Commutative Monoids in Homotopy Type Theory. Electronic Notes in Theoretical Informatics and Computer Science, 1 (2023), https://doi.org/10.46298/entics.10492
[14]
Valeria de Paiva. 2014. Categorical Semantics of Linear Logic for All. Springer Netherlands, Dordrecht. 181–192. isbn:978-94-007-7548-0 https://doi.org/10.1007/978-94-007-7548-0_9
[15]
Thomas Ehrhard and Farzad Jafarrahmani. 2021. Categorical models of Linear Logic with fixed points of formulas. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021. IEEE, 1–13. https://doi.org/10.1109/LICS52264.2021.9470664
[16]
Jean-Yves Girard. 1987. Linear Logic. Theor. Comput. Sci., 50 (1987), 1–102. https://doi.org/10.1016/0304-3975(87)90045-4
[17]
Jason Gross, Adam Chlipala, and David I. Spivak. 2014. Experience Implementing a Performant Category-Theory Library in Coq. In Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, Gerwin Klein and Ruben Gamboa (Eds.) (Lecture Notes in Computer Science, Vol. 8558). Springer, 275–291. https://doi.org/10.1007/978-3-319-08970-6_18
[18]
Jason Z. S. Hu and Jacques Carette. 2021. Formalizing category theory in Agda. In CPP ’21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021, Catalin Hritcu and Andrei Popescu (Eds.). ACM, 327–342. https://doi.org/10.1145/3437992.3439922
[19]
Martin Hyland and Andrea Schalk. 2003. Glueing and orthogonality for models of linear logic. Theor. Comput. Sci., 294, 1/2 (2003), 183–231. https://doi.org/10.1016/S0304-3975(01)00241-9
[20]
Farzad Jafarrahmani. 2023. Fixpoints of Types in Linear Logic from a Curry-Howard-Lambek Perspective. Université Paris Cité, France. https://hal.science/tel-04295098v1
[21]
Yves Lafont. 1988. The Linear Abstract Machine. Theor. Comput. Sci., 59 (1988), 157–180. https://doi.org/10.1016/0304-3975(88)90100-4
[22]
Ugo Dal Lago and Martin Hofmann. 2011. Realizability models and implicit complexity. Theor. Comput. Sci., 412, 20 (2011), 2029–2047. https://doi.org/10.1016/J.TCS.2010.12.025
[23]
Saunders Mac Lane. 1998. Categories for the Working Mathematician (second ed.) (Graduate Texts in Mathematics, Vol. 5). Springer-Verlag, New York. isbn:0-387-98403-8
[24]
The mathlib Community. 2020. The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, Jasmin Blanchette and Catalin Hritcu (Eds.). ACM, 367–381. https://doi.org/10.1145/3372885.3373824
[25]
Ralph Matthes, Kobe Wullaert, and Benedikt Ahrens. 2023. Substitution for Non-Wellfounded Syntax with Binders through Monoidal Categories. CoRR, abs/2308.05485 (2023), https://doi.org/10.48550/ARXIV.2308.05485
[26]
Paul-André Melliès. 2003. Categorical models of linear logic revisited. Oct., https://hal.science/hal-00154229 working paper or preprint
[27]
Paul-André Melliès. 2009. Categorical Semantics of Linear Logic (Panorama & Synthèses, Vol. 27). Société Mathématique de France. https://www.irif.fr/~mellies/papers/panorama-submitted.pdf
[28]
Ulf Norell. 2008. Dependently Typed Programming in Agda. In Advanced Functional Programming, 6th International School, AFP 2008, Heijen, The Netherlands, May 2008, Revised Lectures, Pieter W. M. Koopman, Rinus Plasmeijer, and S. Doaitse Swierstra (Eds.) (Lecture Notes in Computer Science, Vol. 5832). Springer, 230–266. https://doi.org/10.1007/978-3-642-04652-0_5
[29]
Peter W. O’Hearn. 2003. On bunched typing. J. Funct. Program., 13, 4 (2003), 747–796. https://doi.org/10.1017/S0956796802004495
[30]
Erik Palmgren. 2017. On Equality of Objects in Categories in Constructive Type Theory. In 23rd International Conference on Types for Proofs and Programs, TYPES 2017, May 29-June 1, 2017, Budapest, Hungary, Andreas Abel, Fredrik Nordvall Forsberg, and Ambrus Kaposi (Eds.) (LIPIcs, Vol. 104). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 7:1–7:7. https://doi.org/10.4230/LIPIcs.TYPES.2017.7
[31]
Stefano Piceghello. 2021. Coherence for Monoidal and Symmetric Monoidal Groupoids in Homotopy Type Theory. The University of Bergen. isbn:978-82-308-4711-4 https://bora.uib.no/bora-xmlui/handle/11250/2830640
[32]
Gordon D. Plotkin. 1993. Type Theory and Recursion (Extended Abstract). In Proceedings of the Eighth Annual Symposium on Logic in Computer Science (LICS ’93), Montreal, Canada, June 19-23, 1993. IEEE Computer Society, 374. https://doi.org/10.1109/LICS.1993.287571
[33]
R. A. G. Seely. 1989. Linear logic, *-autonomous categories and cofree coalgebras. In Categories in computer science and logic (Boulder, CO, 1987) (Contemp. Math., Vol. 92). Amer. Math. Soc., Providence, RI, 371–382. isbn:0-8218-5100-4 https://doi.org/10.1090/conm/092/1003210
[34]
Eugene W. Stark. 2017. Monoidal Categories. Arch. Formal Proofs, 2017 (2017), https://www.isa-afp.org/entries/MonoidalCategory.shtml
[35]
The Coq Development Team. 2022. The Coq Proof Assistant. https://doi.org/10.5281/zenodo.7313584
[36]
The 1Lab Development Team. [n. d.]. The 1Lab. https://1lab.dev
[37]
Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. 2019. Cubical agda: a dependently typed programming language with univalence and higher inductive types. Proc. ACM Program. Lang., 3, ICFP (2019), 87:1–87:29. https://doi.org/10.1145/3341691
[38]
Vladimir Voevodsky, Benedikt Ahrens, and Daniel Grayson. [n. d.]. UniMath — a computer-checked library of univalent mathematics. Available at. http://unimath.org
[39]
Makarius Wenzel, Lawrence C. Paulson, and Tobias Nipkow. 2008. The Isabelle Framework. In Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, Otmane Aït Mohamed, César A. Muñoz, and Sofiène Tahar (Eds.) (Lecture Notes in Computer Science, Vol. 5170). Springer, 33–38. https://doi.org/10.1007/978-3-540-71067-7_7
[40]
Kobe Wullaert, Ralph Matthes, and Benedikt Ahrens. 2022. Univalent Monoidal Categories. In 28th International Conference on Types for Proofs and Programs, TYPES 2022, June 20-25, 2022, LS2N, University of Nantes, France, Delia Kesner and Pierre-Marie Pédrot (Eds.) (LIPIcs, Vol. 269). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 15:1–15:21. https://doi.org/10.4230/LIPIcs.TYPES.2022.15
Index Terms
- Displayed Monoidal Categories for the Semantics of Linear Logic
Recommendations
Bialgebras in Rel
We study bialgebras in the compact closed category Rel of sets and binary relations. We show that various monoidal categories with extra structure arise as the categories of (co)modules of bialgebras in Rel. In particular, for any group G we derive a ...
Linear-Algebraic Models of Linear Logic as Categories of Modules over Σ-Semirings✱
LICS '22: Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer ScienceA number of models of linear logic are based on or closely related to linear algebra, in the sense that morphisms are “matrices” over appropriate coefficient sets. Examples include models based on coherence spaces, finiteness spaces and probabilistic ...
When does a category built on a lattice with a monoidal structure have a monoidal structure?
In a word, sometimes. And it gets harder if the structure on L is not commutative. In this paper we consider the question of what properties are needed on the lattice L equipped with an operation @? for several different kinds of categories built using ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
January 2024
290 pages
ISBN:9798400704888
DOI:10.1145/3636501
- General Chairs:
- Amin Timany,
- Dmitriy Traytel,
- Program Chairs:
- Brigitte Pientka,
- Sandrine Blazy
Copyright © 2024 Owner/Author.
This work is licensed under a Creative Commons Attribution International 4.0 License.
Sponsors
In-Cooperation
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 09 January 2024
Check for updates
Author Tags
Qualifiers
- Research-article
Funding Sources
Conference
CPP '24
Sponsor:
CPP '24: 13th ACM SIGPLAN International Conference on Certified Programs and Proofs
January 15 - 16, 2024
London, UK
Acceptance Rates
Overall Acceptance Rate 18 of 26 submissions, 69%
Upcoming Conference
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 351Total Downloads
- Downloads (Last 12 months)351
- Downloads (Last 6 weeks)35
Reflects downloads up to 09 Jan 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in