IMELL Cut Elimination with Linear Overhead
arxiv(2024)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要