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.

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.