Accession Number : ADA292248
Title : Structural Cut Elimination in Linear Logic.
Corporate Author : CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
Personal Author(s) : Pfenning, Frank
PDF Url : ADA292248
Report Date : DEC 1994
Pagination or Media Count : 64
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. (AN)
Descriptors : *COMPUTER LOGIC, *STRUCTURED PROGRAMMING, COMPUTER PROGRAM DOCUMENTATION, ALGORITHMS, LINEAR SYSTEMS, COMPUTATIONS, PROGRAMMING LANGUAGES, RULE BASED SYSTEMS, SUBROUTINES, CONTROL SEQUENCES.
Subject Categories : Computer Programming and Software
Distribution Statement : APPROVED FOR PUBLIC RELEASE