[Prev][Next][Index][Thread]

Papers on Cut Elimination



I would like to announce the availability of the following two technical
reports regarding cut elimination in intuitionistic, classical, and linear
logic.  They are summarized in:

  Structural Cut Elimination (extended abstract)
  Frank Pfenning
  December 1994

DVI file:
  file://ftp.cs.cmu.edu/afs/cs/user/fp/public/papers/cutstruct94.dvi.Z
Implementation:
  file://ftp.cs.cmu.edu /afs/cs/user/fp/public/elf-papers/cutstruct94.tar.Z

All papers are also accessible through my home page on the world-wide
web.

  - Frank
----------------------------------------------------------------------
Frank Pfenning                      Telephone: +1 412 268-6343       
Department of Computer Science            FAX: +1 412 268-5576       
Carnegie Mellon University           InterNet: fp@cs.cmu.edu         
Pittsburgh, PA 15213-3891, U.S.A.    
Web: http://www.cs.cmu.edu:8001/afs/cs/user/fp/www/homepage.html
----------------------------------------------------------------------
Frank Pfenning.  Structural cut elimination in linear logic.
Technical Report CMU-CS-94-222, Department of Computer Science,
Carnegie Mellon University, December 1994.

ABSTRACT:

 We present a new proof of cut elimination for linear logic which proceeds by
three 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.

PostScript:
 file://ftp.cs.cmu.edu/afs/cs/user/fp/public/papers/cutlin94.ps.Z
Implementation:
 file://ftp.cs.cmu.edu/afs/cs/user/fp/public/elf-papers/cutlin94.tar.Z

--------------------------------------------------
Frank Pfenning.  A structural proof of cut elimination and its
representation in a logical framework.
Technical Report CMU-CS-94-218, Department of Computer Science,
Carnegie Mellon University, November 1994.

ABSTRACT:

 We present new proofs of cut elimination for intuitionistic and classical
sequent calculi.  In both 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
representations in LF, which are given in full detail.

PostScript:
 file://ftp.cs.cmu.edu/afs/cs/user/fp/public/papers/cutelim94.ps.Z
Implementation:
 file://ftp.cs.cmu.edu/afs/cs/user/fp/public/elf-papers/cutelim94.tar.Z