# Proof Diagrams for Multiplicative Linear Logic: Syntax and Semantics

## TL;DR

This paper introduces a 2-dimensional proof diagram syntax for multiplicative linear logic that simplifies correctness verification and provides a new denotational semantics via proof diagram equivalence classes.

## Contribution

It presents an alternative geometrical proof syntax using string diagrams, enabling linear-time correctness checking and a novel semantics for multiplicative linear logic with units.

## Key findings

- Linear-time correctness verification for proof diagrams.
- A new denotational semantics based on proof diagram equivalence classes.
- An alternative to traditional proof nets with geometrical intuition.

## Abstract

Proof nets are a syntax for linear logic proofs which gives a coarser notion of proof equivalence with respect to syntactic equality together with an intuitive geometrical representation of proofs. In this paper we give an alternative $2$-dimensional syntax for multiplicative linear logic derivations. The syntax of string diagrams authorizes the definition of a framework where the sequentializability of a term, i.e. deciding whether the term corresponds to a correct derivation, can be verified in linear time. Furthermore, we can use this syntax to define a denotational semantics for multiplicative linear logic with units by means of equivalence classes of proof diagrams modulo a terminating rewriting.

---
Source: https://tomesphere.com/paper/1702.00268