Title :
Structural cut elimination
Author_Institution :
Dept. of Comput. Sci., Carnegie Mellon Univ., Pittsburgh, PA, USA
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;
Conference_Titel :
Logic in Computer Science, 1995. LICS '95. Proceedings., Tenth Annual IEEE Symposium on
Conference_Location :
San Diego, CA
Print_ISBN :
0-8186-7050-9
DOI :
10.1109/LICS.1995.523253
