POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Tue 16 Jan 2024 11:00 - 11:30 at Kelvin Lecture - Formalizations of Category Theory Chair(s): Robert Atkey

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.

Tue 16 Jan

Displayed time zone: London change

11:00 - 12:30
Formalizations of Category TheoryCPP at Kelvin Lecture
Chair(s): Robert Atkey University of Strathclyde
11:00
30m
Talk
Displayed Monoidal Categories for the Semantics of Linear Logic
CPP
Benedikt Ahrens Delft University of Technology, Ralph Matthes IRIT, Université de Toulouse, CNRS, Toulouse INP, UT3, Toulouse, Niels van der Weide Radboud University, Kobe Wullaert Delft University of Technology
11:30
30m
Talk
Univalent Double Categories
CPP
Niels van der Weide Radboud University, Nima Rasekh Max Planck Institute for Mathematics, Benedikt Ahrens Delft University of Technology, Paige Randall North Utrecht University
12:00
30m
Talk
Formalizing the ∞-categorical Yoneda lemma
CPP
Nikolai Kudasov Innopolis University, Emily Riehl Johns Hopkins University, Jonathan Weinberger Johns Hopkins University
Link to publication DOI Pre-print