![[Search]](/static/images/search.gif){kind=small}
![[A-Z Index]](/static/images/az.gif){kind=small}
![[Contact]](/static/images/contact.gif){kind=small}
![[University of Cambridge]](/static/images/identifier2.gif){kind=small}
![[Talks.cam]](/static/images/talkslogosmall.gif)
Federico Olimpieri, University of Leeds
Friday 20 October 2023, 14:00-15:00
Coherence by Normalization for Linear Multicategorical Structures
- đ¤ Speaker: Federico Olimpieri, University of Leeds
- đ Date & Time: Friday 20 October 2023, 14:00 - 15:00
- đ Venue: SS03, Computer Laboratory
Abstract
We establish a formal correspondence between resource calculi and appropriate linear multicategories. We consider the cases of (symmetric) representable, symmetric closed and autonomous multicategories. For all these structures, we prove that morphisms of the corresponding free constructions can be presented by means of typed resource terms, up to a reduction relation and a structural equivalence. Thanks to the linearity of the calculi, we can prove strong normalization of the reduction by combinatorial methods, defining appropriate decreasing measures. From this, we achieve a general coherence result: morphisms that live in the free multicategorical structures are the same whenever the normal forms of the associated terms are equal. As further application, we obtain syntactic proofs of Mac Lane’s coherence theorems for (symmetric) monoidal categories.
Series This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.
Included in Lists
- All Talks (aka the CURE list)
- bld31
- Cambridge talks
- Computing and Mathematics
- Department of Computer Science and Technology talks and seminars
- Interested Talks
- Logic and Semantics Seminar (Computer Laboratory)
- Martin's interesting talks
- School of Technology
- SS03, Computer Laboratory
- tcw57âs list
- Trust & Technology Initiative - interesting events
- yk373's list
- yk449
Note: Ex-directory lists are not shown.