Coherence for Frobenius pseudomonoids and the geometry of linear proofs
Research output: Contribution to journal › Article › peer-review
Standard
Coherence for Frobenius pseudomonoids and the geometry of linear proofs. / Dunn, Lawrence ; Vicary, Jamie.
In: Logical Methods in Computer Science, Vol. 15, No. 3, 26.07.2019.Research output: Contribution to journal › Article › peer-review
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
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
VL - 15
JO - Logical Methods in Computer Science
JF - Logical Methods in Computer Science
SN - 1860-5974
IS - 3
ER -