Gentzen-Style Classical Proofs as λµ-Terms

We show that one can consider the Gentzenstyle classical logic LKT, as presented in Danos et al.(1993), can be considered as the classical call-by-name (CBN) calculus. First, we present a new term calculus for LKT which is isomorphic to cut-elimination procedure (tq-protocol) for LKT. Then, we present a translation of Parigot's λµ-calculus into our term calculus. This translation is essentially identical with so-called Continuation Passing Style. Using this translation, one can show that LKT correctly simulates λµ-calculus. Specifically the Strongly Normalizable(SN) and Church-Rosser(CR) property of λµ-calculus is shown to be a consequence of the SN and CR property of tq-protocol for LKT