IMELL Cut Elimination with Linear Overhead
<|reference_start|>IMELL Cut Elimination with Linear Overhead: 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.<|reference_end|>
@article{accattoli2024imell,
    title={IMELL Cut Elimination with Linear Overhead},
    author={Beniamino Accattoli, Claudio Sacerdoti Coen},
    journal={arXiv preprint arXiv:2405.03669},
    year={2024},
    archivePrefix={arXiv},
    eprint={2405.03669},
    primaryClass={cs.LO}
}