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.

翻译：使用续延编译的本质在于：将程序转换为续延传递风格（CPS）等价于一种源语言转换，该转换将其转化为管理正常形式（ANF）。以Moggi的计算λ-演算（lbc）作为源语言，我们定义了一种替代CPS翻译的方法，其目标语言为相继式演算LJQ，称为值填充风格（VFS）翻译，该方法利用了相继式演算在形式上表示上下文的能力。VFS翻译无需类型翻译：实际上，双重否定仅在将VFS目标语言编码为CPS目标语言时引入。这种可选编码在与VFS翻译组合时，重构了原始的CPS翻译。回归直接风格后，VFS翻译的“本质”在于揭示了ANF的一个新子语言——值封闭风格（VES），以及另一子语言——续延封闭风格（CES）：这种替代源于lbc语法中关于如何扩展应用构造子的一个二难困境。在有类型场景下，VES和CES对应按值调用的两种证明系统——LJQ和带广义应用的自然演绎，从而确认了证明论作为中间表示的基础。