IMELL Cut Elimination with Linear Overhead

TL;DR

This paper refines previous work on IMELL cut elimination by introducing an abstract machine that implements a strategy with linear overhead, improving efficiency in proof normalization.

Contribution

It introduces an abstract machine for ESC that executes the good cut elimination strategy with linear overhead, enhancing the computational model for IMELL.

Findings

The machine implements the good strategy effectively.

Cut elimination is achieved with linear overhead.

The approach improves the efficiency of proof normalization.

Abstract

Recently, Accattoli introduced the Exponential Substitution Calculus (ESC) given by untyped proof terms for Intuitionistic Multiplicative Exponential Linear Logic (IMELL), endowed with rewriting rules at-a-distance for cut elimination. He also introduced a new cut elimination strategy, dubbed the good strategy, and showed that its number of steps is a time cost model with polynomial overhead for the ESC/IMELL, and the first such one. Here, we refine Accattoli's result by introducing an abstract machine for ESC and proving that it implements the good strategy and computes cut-free terms/proofs within a linear overhead.