Structural Cut Elimination in Linear Logic

摘要

We present a new proof of cut elimination for linear logic which proceeds bythree nested structural inductions, avoiding the explicit use of multi-sets and termination measures on sequent derivations. The computational content of this proof is a non-deterministic algorithm for cut elimination which is amenable to an elegant implementation in Elf. We show this implementation in detail. (AN).