DocumentCode
3292507
Title
Structural cut elimination
Author
Pfenning, Frank
Author_Institution
Dept. of Comput. Sci., Carnegie Mellon Univ., Pittsburgh, PA, USA
fYear
1995
fDate
26-29 Jun 1995
Firstpage
156
Lastpage
166
Abstract
Presents 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
Keywords
constraint handling; process algebra; programming theory; Elf; LF logical framework; classical sequent calculus; constraint logic programming language; cut admissibility; intuitionistic sequent calculus; linear sequent calculus; nested structural inductions; structural cut elimination; Application software; Calculus; Computer science; Constraint theory; Data structures; Logic programming;
fLanguage
English
Publisher
ieee
Conference_Titel
Logic in Computer Science, 1995. LICS '95. Proceedings., Tenth Annual IEEE Symposium on
Conference_Location
San Diego, CA
ISSN
1043-6871
Print_ISBN
0-8186-7050-9
Type
conf
DOI
10.1109/LICS.1995.523253
Filename
523253
Link To Document