Structural Cut Elimination in Linear Logic.

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)

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Dec 01, 1994
Accession Number
ADA292248

Entities

People

  • Frank Pfenning

Organizations

  • Carnegie Mellon University

Tags

DTIC Thesaurus Topics

  • Additives (Chemicals)
  • Algorithms
  • Ambiguity
  • Calculus
  • Coding
  • Computations
  • Computer Programming
  • Computer Science
  • Computers
  • Crossings
  • Elimination
  • Hypotheses
  • Judgment
  • Language
  • Notation
  • Programming Languages
  • Theoretical Computer Science

Fields of Study

  • Computer science

Readers

  • Applied Combinatorial Optimization and Logic Circuit Design.
  • Graph Algorithms and Convex Optimization.
  • Parallel and Distributed Computing.