Displayed Monoidal Categories for the Semantics of Linear Logic

Title

Displayed Monoidal Categories for the Semantics of Linear Logic

 Author

Ahrens, B.P. (TU Delft Programming Languages; University of Birmingham)
Matthes, Ralph (INPT; Université de Toulouse)
van der Weide, N.J. (Radboud Universiteit Nijmegen)
Wullaert, K.F. (TU Delft Programming Languages)

Contributor

Timany, Amin (editor)
Traytel, Dmitriy (editor)
Pientka, Brigitte (editor)
Blazy, Sandrine (editor)

Date

2024

 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.


 Subject

categorical semantics
Coq
linear logic
monoidal categories
UniMath

 To reference this document use:

http://resolver.tudelft.nl/uuid:4fed6676-a637-4bbb-9212-20704504cc2e

 DOI

https://doi.org/10.1145/3636501.3636956

 Publisher

Association for Computing Machinery (ACM), New York, NY, USA

 ISBN

979-8-4007-0488-8

 Source

CPP 2024 - Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs

 Event

13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, in affiliation with the annual Symposium on Principles of Programming, Languages, ,POPL 2024, 2024-01-15 → 2024-01-16, London, United Kingdom

 Part of collection

Institutional Repository

 Document type

conference paper

 Rights

© 2024 B.P. Ahrens, Ralph Matthes, N.J. van der Weide, K.F. Wullaert
Files
PDF 3636501.3636956.pdf 415.43 KB
Close viewer