CiteSeerX - Document Details (Isaac Councill, Lee Giles, Pradeep Teregowda): . We show that the one can consider proof of the Gentzen's LK  as the continuation passing style(CPS) programs; and the cut-elimination procedure for LK as computation. To be more precise, we observe that Strongly Normalizable(SN) and Church-Rosser(CR) cut-elimination procedure for (intuitionistic decoration of) LKT and LKQ, as presented in Danos et al.(1993), precisely corresponds to call-by-name(CBN) and call-by-value(CBV) CPS calculi, respectively. This can also be seen as an extension to classical logic of Zucker-Pottinger-Mints investigation of the relations between cut-elimination and normalization. 1 Introduction  Continuation Passing Style(CPS): Since Griffin's influential work [12] on the Curry-Howard correspondence between classical proofs and CPS programs, there has been a lot of interest on programming in classical proofs. It is because these classical calculi relate to important programming concepts such as non-local exit…