[L3] ================================================ AMAST Links 02 02

                 Two Papers regarding Cut Elimination
                           by Frank Pfenning

   The _full version_ of this contribution is available at
URL: http://www.cs.utwente.nl/data/amast/links/v02/i02/full/CE2Pl.txt

  This is to announce two papers regarding cut elimination in 
intuitionistic, classical, and linear logic.  They are summarized in:
_Structural Cut Elimination_ (extended abstract), Frank Pfenning, 
December 1994, which is available by _anonymous ftp_ at URL: 
ftp://ftp.cs.cmu.edu/afs/cs/user/fp/public/papers/cutstruct94.dvi.Z
  All papers are also accessible through WWW at
URL: http://www.cs.cmu.edu:8001/afs/cs/user/fp/www/homepage.html

**Structural cut elimination in linear logic**

  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.

**A structural proof of cut elimination and its representation in a 
logical framework**

  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.