Proof Diagrams for Multiplicative Linear Logic: Syntax and Semantics

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.

pre-print, submitted

References in corpus (6)

• A survey of graphical languages for monoidal categories
• A Prehistory of n-Categorical Physics
• Termination orders for 3-dimensional rewriting
• Higher-dimensional categories with finite derivation type
• A Constructive Proof of Coherence for Symmetric Monoidal Categories Using Rewriting
• Proof Diagrams for Multiplicative Linear Logic

Cited by in corpus (3)

• Deconstructing the Calculus of Relations with Tape Diagrams
• Computational Complexity of Deciding Provability in Linear Logic and its Fragments
• Exponentially Handsome Proof Nets and Their Normalization