Coherence for Frobenius pseudomonoids and the geometry of linear proofs

Research output: Contribution to journalArticlepeer-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 journalArticlepeer-review

Harvard

APA

Vancouver

Author

Bibtex

@article{06fb2821914043939c84b5b8f26f4baf,
title = "Coherence for Frobenius pseudomonoids and the geometry of linear proofs",
abstract = "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.",
author = "Lawrence Dunn and Jamie Vicary",
year = "2019",
month = jul,
day = "26",
doi = "10.23638/LMCS-15(3:5)2019",
language = "English",
volume = "15",
journal = "Logical Methods in Computer Science",
issn = "1860-5974",
publisher = "IfCoLog",
number = "3",

}

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 -