Paper: Structural Cut Elimination (at LICS 1995)

Authors: Frank Pfenning

Abstract

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.

BibTeX

  @InProceedings{Pfenning-StructuralCutElimin,
    author = 	 {Frank Pfenning},
    title = 	 {Structural Cut Elimination},
    booktitle =  {Proceedings of the Tenth Annual IEEE Symposium on Logic in Computer Science (LICS 1995)},
    year =	 {1995},
    month =	 {June}, 
    pages =      {156--166},
    location =   {San Diego, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }