A New Linear Time Correctness Condition for Multiplicative Linear Logic

TL;DR

This paper introduces a simple, efficient linear time correctness condition for proof nets in Multiplicative Linear Logic without units, based on a rewriting system over trees.

Contribution

It presents a novel, straightforward rewriting-based correctness criterion that improves upon previous methods in simplicity and intuitiveness.

Findings

Achieves linear time verification of proof net correctness

Uses only three rewrite rules for the system

Simplifies the process compared to prior conditions

Abstract

In this paper, we give a new linear time correctness condition for proof nets of Multiplicative Linear Logic without units. Our approach is based on a rewriting system over trees. We have only three rewrite rules. Compared with previous linear time correctness conditions, our system is surprisingly simple and intuitively appealing.