loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
10th Annual IEEE Symposium on Logic in Computer Science (LICS'95)
Structural Cut Elimination
San Diego, California
June 26-June 29
ISBN: 0-8186-7050-6
ASCII Text
x 
 
Frank Pfenning, "Structural Cut Elimination," Logic in Computer Science, Symposium on, pp. 156, 10th Annual IEEE Symposium on Logic in Computer Science (LICS'95), 1995.
 
 
BibTex
x
 
@article{ 10.1109/LICS.1995.523253,
author = {Frank Pfenning},
title = {Structural Cut Elimination},
journal ={Logic in Computer Science, Symposium on},
volume = {0},
year = {1995},
issn = {1043-6871},
pages = {156},
doi = {http://doi.ieeecomputersociety.org/10.1109/LICS.1995.523253},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Logic in Computer Science, Symposium on
TI - Structural Cut Elimination
SN - 1043-6871
SP
EP
A1 - Frank Pfenning,
PY - 1995
KW - Logic
KW - Cut Elimination
KW - Logical Framework
KW - Linear Logic
VL - 0
JA - Logic in Computer Science, Symposium on
ER -
 
Frank Pfenning, Department of Computer Science Carnegie Mellon University, Pennsylvania
We present new proofs of cut elimination for intuitionistic, classical, and linear sequent calculi. In all 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 implementations in Elf, a constraint logic programming language based on the LF logical framework.
Index Terms:
Logic, Cut Elimination, Logical Framework, Linear Logic
Citation:
Frank Pfenning, "Structural Cut Elimination," lics, pp.156, 10th Annual IEEE Symposium on Logic in Computer Science (LICS'95), 1995
Usage of this product signifies your acceptance of the Terms of Use.