Recently, the authors identified the “logical essence” of the call-by-value CPS translation to be its decomposition into two translations: a map into a fragment of the sequent calculus LJQ already determining the same semantics as CPS; and a later, optional, “negative” encoding of the referred fragment into the CPS target, responsible for (and requiring) the introduction of double negations. In this paper we analyze how much of this architecture applies to call-by-name CPS translations. We take the most common translation, essentially due to Plotkin, and use the sequent calculus LJT. A similar decomposition holds again, with the CPS semantics already obtained by the translation into the sequent calculus. The perfect match, obtained by the negative encoding, between the sequent calculus and the CPS target is somewhat stronger than the call-by-value case, since it holds both before and after optimizing the CPS translation (by doing administrative reduction on the fly). The optimized CPS target is isomorphic to the source language: there is no call-by-name administrative normal form. Finally, we insert in the picture Hofmann-Streicher CPS translation. In the “positive” translation of the CPS target, back to the negation-free sequent calculus, the HS target can be used as a stepping stone: first, some negations are spared by the use of conjunction; next, the right introduction of conjunction is encoded by the left introduction of implication.

The essence of compiling with continuations is that conversion to continuation-passing style (CPS) is equivalent to a source language transformation converting to administrative normal form (ANF). Taking as source language Moggi's computational lambda-calculus (lbc), we define an alternative to the CPS-translation with target in the sequent calculus LJQ, named value-filling style (VFS) translation, and making use of the ability of the sequent calculus to represent contexts formally. The VFS-translation requires no type translation: indeed, double negations are introduced only when encoding the VFS target language in the CPS target language. This optional encoding, when composed with the VFS-translation reconstructs the original CPS-translation. Going back to direct style, the "essence" of the VFS-translation is that it reveals a new sublanguage of ANF, the value-enclosed style (VES), next to another one, the continuation-enclosing style (CES): such an alternative is due to a dilemma in the syntax of lbc, concerning how to expand the application constructor. In the typed scenario, VES and CES correspond to an alternative between two proof systems for call-by-value, LJQ and natural deduction with generalized applications, confirming proof theory as a foundation for intermediate representations.