IMELL Cut Elimination with Linear Overhead

2024/05/06 by Accattoli, Beniamino, Coen, Claudio Sacerdoti · 1 citation
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.2405.03669

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.

Cited by

• The Cost of Skeletal Call-by-Need, Smoothly

Related

• Linear Logic Properly Displayed
• Reconciling Lambek's restriction, cut-elimination, and substitution in the presence of exponential modalities
• Elimination and cut-elimination in multiplicative linear logic
• A uniform cut-elimination theorem for linear logics with fixed points and super exponentials
• A type-assignment of linear erasure and duplication