Surface proofs for nonsymmetric linear logic
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.
| Main Authors: | , |
|---|---|
| Format: | Conference item |
| Published: |
2016
|
| Summary: | 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. |
|---|