  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.
