Structural Cut Elimination

13 years 9 months ago
Structural Cut Elimination
We present new proofs of cut elimination for intuitionistic, classical, and linear sequent calculi. In all cases the proofs proceed by three nested structural inductions, avoiding the explicit use of multi-sets and termination measures on sequent derivations. This makes them amenable to elegant and concise implementations in Elf, a constraint logic programming language based on the LF logical framework.
Frank Pfenning
Added 26 Aug 2010
Updated 26 Aug 2010
Type Conference
Year 1995
Where LICS
Authors Frank Pfenning
Comments (0)