Terms for Natural Deduction, Sequent Calculus and Cut Elimination in Classical Logic
This paper revisits the results of Barendregt and Ghilezan  and generalizes them for classical logic. Instead of lambda-calculus, we use here lambda-mu-calculus as the basic term calculus. We consider two extensionally equivalent type assignment systems for lambda-mu-calculus, one corresponding to classical natural deduction, and the other to classical sequent calculus. Their relations and normalisation properties are investigated. As a consequence a short proof of Cut elimination theorem is obtained.