A Proof Theoretical Account of Continuation Passing Style

We study "classical proofs as programs" paradigm in CallBy -Value (CBV) setting. Specifically, we show the CBV normalization for CND (Parigot 92) can be simulated by the cut-elimination procedure for LKQ (Danos-Joinet-Schellinx 93), namely the q-protocol. We use proof-term assignment system to prove this fact. The term calculus for CND we use follows Parigot's #-calculus with new CBV normalization procedure. A new term calculus for LKQ is presented as a variant of #-calculus with a let-construct. We then define a translation from CND into LKQ and prove simulation theorem. We also show the translation we use can be thought of a familiar CBV CPS-translation without translation on types.