Surface proofs for linear logic.
Lawrence H. Dunn, Jamie Vicary · arXiv (Cornell University) · 2016
We show that a proof in multiplicative linear logic can be represented as a decorated surface, such that two proofs are logically equivalent just when their surfaces are geometrically equivalent. The technical basis is a coherence theorem for Frobenius pseudomonoids.