This paper introduces the exponential substitution calculus (ESC), a new presentation of cut elimination for IMELL, based on proof terms and building on the idea that exponentials can be seen as explicit substitutions. The idea in itself is not new, but here it is pushed to a new level, inspired by Accattoli and Kesner's linear substitution calculus (LSC). One of the key properties of the LSC is that it naturally models the sub-term property of abstract machines, that is the key ingredient for the study of reasonable time cost models for the $\lambda$-calculus. The new ESC is then used to design a cut elimination strategy with the sub-term property, providing the first polynomial cost model for cut elimination with unconstrained exponentials. For the ESC, we also prove untyped confluence and typed strong normalization, showing that it is an alternative to proof nets for an advanced study of cut elimination.

翻译：本文提出了指数替换演算（ESC），这是基于证明项且利用指数可视为显式替换这一思想的一种新的IMELL割消去表示。该思想本身并不新颖，但受Accattoli和Kesner的线性替换演算（LSC）启发，在此被推向新高度。LSC的关键性质之一是其自然建模抽象机器的子项性质，而这正是研究λ-演算合理时间代价模型的核心要素。随后，新提出的ESC被用于设计具有子项性质的割消去策略，从而为无约束指数的割消去提供了首个多项式代价模型。对于ESC，我们还证明了无类型合流性与有类型强规范化，表明它是用于深耕割消去研究的证明网的一种替代方案。