TY - JOUR
T1 - Coherence for Frobenius pseudomonoids and the geometry of linear proofs
AU - Dunn, Lawrence
AU - Vicary, Jamie
PY - 2019/7/26
Y1 - 2019/7/26
N2 - We prove coherence theorems for Frobenius pseudomonoids and snakeorators in monoidal bicategories. As a consequence we obtain a 3d notation for proofs in nonsymmetric multiplicative linear logic, with a geometrical notion of equivalence, and without the need for a global correctness criterion or thinning links. We argue that traditional proof nets are the 2d projections of these 3d diagrams.
AB - We prove coherence theorems for Frobenius pseudomonoids and snakeorators in monoidal bicategories. As a consequence we obtain a 3d notation for proofs in nonsymmetric multiplicative linear logic, with a geometrical notion of equivalence, and without the need for a global correctness criterion or thinning links. We argue that traditional proof nets are the 2d projections of these 3d diagrams.
U2 - 10.23638/LMCS-15(3:5)2019
DO - 10.23638/LMCS-15(3:5)2019
M3 - Article
SN - 1860-5974
VL - 15
JO - Logical Methods in Computer Science
JF - Logical Methods in Computer Science
IS - 3
ER -