We study the "classical proofs as programs" paradigm in Call-By-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 a proof-term assignment system to prove this fact. The term calculus for CND we use follows Parigot's λμ-Calculus and is closely related to Ong-Stewart's(Ong-Stewart 97). 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.
展开▼
