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.

翻译：最近，Accattoli引入了指数代换演算（Exponential Substitution Calculus, ESC），该演算通过无类型证明项为直觉乘法指数线性逻辑（Intuitionistic Multiplicative Exponential Linear Logic, IMELL）提供支持，并配备了用于切割消除的远距离重写规则。他还提出了一种新的切割消除策略（称为“优良策略”），并证明其步数构成了ESC/IMELL的多项式开销时间成本模型，且为首次提出的此类模型。本文通过为ESC引入一台抽象机，并证明该抽象机实现了优良策略且能以线性开销计算无切割项/证明，从而改进了Accattoli的结果。