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