Shifting the Stage
Staging with Delimited Control
Yukiyoshi Kameyama

Oleg Kiselyov

Chung-chieh Shan

University of Tsukuba
kameyama@acm.org

FNMOC
oleg@pobox.com

Rutgers University
ccshan@cs.rutgers.edu

Abstract
It is often hard to write programs that are efficient yet reusable.
For example, an efficient implementation of Gaussian elimination
should be specialized to the structure and known static propertiesof the input matrix. The most profitable optimizations, such as
choosing the best pivoting or memoization, cannot be expected ofeven an advanced compiler because they are specific to the domain,
but expressing these optimizations directly makes for ungainly
source code. Instead, a promising and popular way to reconcile
efficiency with reusability is for a domain expert to write code
generators.
Two pillars of this approach are types and effects. Typed multilevel languages such as MetaOCaml ensure safety: a well-typed
code generator neither goes wrong nor generates code that goes
wrong. Side effects such as state and control ease correctness: aneffectful generator can resemble the textbook presentation of analgorithm, as is familiar to domain experts, yet insert let for memoization and if for bounds-checking, as is necessary for efficiency.
However, adding effects blindly renders multilevel types unsound.
We introduce the first two-level calculus with control effects anda sound type system. We give small-step operational semantics aswell as a continuation-passing style (CPS) translation. For soundness, our calculus restricts the code generator’s effects to the scopeof generated binders. Even with this restriction, we can finally write
efficient code generators for dynamic programming and numericalmethods in direct style, like in algorithm textbooks, rather than in
CPS or monadic style.
Categories and Subject Descriptors D.3.1 [Programming Languages]: Formal Definitions and Theory; D.3.3 [Programming
Languages]: Language Constructs and Features—Control structures; F.3.3 [Logics and Meanings of Programs]: Studies of Program Constructs—Type structure
General Terms Design, Languages
Keywords Staged programming, multilevel languages, code generation, mutable state, delimited control, side effects, continuations

1.

Introduction

High-performance computing and high-assurance embedded computing often call for programs that are specialized for particular

Permission to make digital or hard copies of all or part of this work for personal orclassroom use is granted without fee provided that copies are not made or distributedfor profit or commercial advantage and that copies bear this notice and the full citationon the first page. To copy otherwise, to republish, to post on servers or to redistributeto lists, requires prior specific permission and/or a fee.
PEPM’09, January 19–20, 2009, Savannah, Georgia, USA.
Copyright c 2009 ACM 978-1-60558-327-3/09/01. . . $5.00

inputs, usages, or processors. Writing such programs by hand islabor-intensive and error-prone. In contrast, code generation offers
a promising approach that reconciles modularity and abstraction
with efficiency and safety: the programmer can write a generic program that generates specialized code and assures it safe (Hammondand Michaelson 2003; Püschel et al. 2005).
It is attractive to implement such a code generator in a multilevel language (Gomard and Jones 1991; Nielson and Nielson
1988, 1992) such as MetaOCaml (2006; Lengauer and Taha 2006),
because a multilevel language offers a principled interface to a code
generator for building and composing code fragments and manipulating their binding structure. The interface can guarantee thatthe generated code is syntactically well-formed, even well-typed
and well-scoped. Multilevel languages are thus popular in applications of code generation such as partial evaluation (Gomard andJones 1991), continuation-passing style (CPS) translation (Danvy
and Filinski 1992), embedding domain-specific languages (DSLs)(Czarnecki et al. 2004; Pašalić et al. 2002), and controlling special
processors (Elliott 2004; Taha 2005).
In domains whose experts are not well-versed in programminglanguage research, code generation can only deliver its promise if acode generator is almost as easy for a domain expert to implement
as an unspecialized algorithm. Multilevel languages have gone along way towards this goal, but not enough yet. For example, using a multilevel language to generate specialized code improves
the performance and assurance of dynamic programming (Swadi
et al. 2006) as well as Gaussian elimination (Carette and Kiselyov2008), but current multilevel languages leave us with an agonizing tradeoff: our generators must either be written in CPS (Bondorf 1992; Danvy and Filinski 1990, 1992) or monadic style (Swadi
et al. 2006), or use delimited control operators (Danvy and Filinski
1990, 1992; Lawall and Danvy 1994) or mutable state (Sumii andKobayashi 2001). The first choice renders the code generators inscrutable to the typical programmer who learned unspecialized algorithms from a numerical-methods textbook, whereas the second
choice voids the multilevel language’s guarantee that the generated
code is well-formed. In short, we cannot achieve clarity, safety, andefficiency at the same time.
Contributions Motivated by this agony, this paper introduces λ1 ,the first two-level language with delimited control operators thatassures in its type system that all generated code is well-typed andwell-scoped. The main innovation of the language is to maintaintype soundness by restricting side effects incurred during code generation to the scope of generated binders. We have embedded thelanguage in MetaOCaml, where the restriction has to be checked
manually, and implemented it fully in Twelf. The language is aα (Kameyama et al. 2008), and thesmall, simplified variant of λ1v
restriction on effects is also simple. Nevertheless, we can express
code generators that perform let- and if -insertion—including Gaussian elimination and dynamic programming—in direct style rather

than resorting to CPS or monadic style. We can thus use our new
language to create frameworks and embedded DSLs for program
generation that application programmers and domain experts canuse. Our implementations of λ1 and of direct-style code generators, including the examples of the dynamic programming specialization benchmark (Swadi et al. 2005), are all available online at
http://okmij.org/ftp/Computation/staging/README.dr.
Organization Section 2 illustrates the challenges of code generation using the Gibonacci function in MetaOCaml. Section 3 introduces our new language, shows how its combination of delimited
control and staging meets the challenges, and explains its type system. Section 4 proves that the type system is sound and delivers
principal types. Section 5 presents a CPS translation for the language. Section 6 discusses related work, and Section 7 concludes.

2.

Running example

Our running example is the Gibonacci function in the dynamic programming specialization benchmark (Swadi et al. 2005). It generalizes the Fibonacci function and can be written in OCaml as follows.
let rec gib x y n =if n = 0 then x else
if n = 1 then y else
gib x y (n-1) + gib x y (n-2)
There are better ways of computing Gibonacci—after all, there exists a closed formula. The code above, however, is only slightly
simpler than the serious examples of dynamic programming foundin the benchmark, such as longest common subsequence, binary
knapsack, and optimal matrix multiplication ordering. Optimal
staging of the longest common subsequence is described in Appendix A; the accompanying code deals with other examples.
To generate specialized versions of gib when the argument n is
statically known, we can write the following MetaOCaml code.
(* val gibgen: int code -> int code -> int -> int code *)let rec gibgen x y n =if n = 0 then x else
if n = 1 then y else.<.~(gibgen x y (n-1)) + .~(gibgen x y (n-2))>.
let test_gibgen n =.<fun x y -> .~(gibgen .<x>. .<y>. n)>.
A pair of brackets .<e>. encloses a future-stage expression e,
which is a fragment of generated code. Whereas 1 + 2 is a presentstage expression of type int, .<1 + 2>. is a present-stage valueof type int code, containing the code to add two integers.1 To
combine code values, we use escapes .~e within brackets. The
escaped expression e is evaluated at the present stage; its result,which must be a code value, is spliced into the enclosing bracket.
The inferred type of gibgen above describes it as a code generator
that takes two code values as arguments (even open code values
such as .<x>. and .<y>.). Brackets and escapes in MetaOCaml
are thus equivalent to next and prev in λ (Davies 1996). They
are similar to quasiquote and unquote in Lisp, except a futurestage binder such as fun x above generates a new name and binds
it in a single operation, so no generator (even if ill-typed) everproduces ill-scoped code. For example, to specialize gib to the caseof n being 5, we evaluate test_gibgen 5 to yield the value.<fun x_1 -> fun y_2 ->((((y_2 + x_1) + y_2) + (y_2 + x_1)) +((y_2 + x_1) + y_2))>.
1 This expression actually has the type (’a,int)

code in MetaOCaml,
where the type variable ’a is an environment classifier (Taha and Nielsen2003). Classifiers are not needed in this paper (see §3.1), so we elide them.

in which MetaOCaml generates the names x_1 and y_2 fresh. This
code value has the type (int -> int -> int) code. Besides
printing it, MetaOCaml can compile it into independently usable C
or Fortran code (Eckhardt et al. 2005) or run it.
2.1

Memoization

The naively specialized gib code is patently inefficient like gib
itself: the computation y_2 + x_1 is repeated thrice. Gibonacci,
as with dynamic programming algorithms, can be greatly sped up
by memoization (Michie 1968), a form of information propagation(Sørensen et al. 1994).
The most appealing memoization method requires minimalchanges in the code. The programmer only needs to rewrite thecode to ‘open up the recursion’:let gib x y self n =if n = 0 then x else
if n = 1 then y else
self (n-1) + self (n-2)
The function gib is no longer recursive. It receives an extra argument self for the recursive instance of itself. We ‘tie the knot’ withthe explicit fixpoint combinator y_simple:
let rec y_simple f n = f (y_simple f) n
Evaluating y_simple (gib 1 1) 5 yields 8 in the same inefficient way as before. To add memoization, we switch to a different fixpoint combinator y_memo_m, but keep the same gib code
(McAdam 2001).
let y_memo_m f n =let table = ref (empty ()) in
let rec memo n =match (lookup n !table) with
| None -> let v = f memo n in(table := ext !table n v; v)| Some v -> v
in f memo n
Just as the definition of gib closely follows how a textbook
might describe the Gibonacci function, the definition of y_memo_mclosely follows how a textbook might describe memoization. We
assume a finite-map data-type with the operations empty () tocreate the empty map, lookup n table to locate a value associated with the integer key n, and ext table n v to return a newmap extending table by associating the key n to the value v. Now
we can evaluate y_memo_m (gib 1 1) 30, which finishes much
faster than y_simple (gib 1 1) 30.
This memoization method is appealing because it relegatesmemoization to a library of fixpoint combinators and does not
distort the code of the algorithm (gib in our case). In a support
library for dynamic programming (which was the goal of Swadi
et al. (2006)), this method allows application programmers to write
natural and modular code, implementing memoization strategies
separately from functions to memoize.
However, this simple method does not work when specializing
gib, for two reasons. First, the memoizing combinator y_memo_mmust use mutation so that the two sibling calls to self in gib, withno explicit data flow between them, could reuse each other’s computation by sharing the same memoization table. When specializing
memoized gib, the table stores code values. Alas, blindly combining mutation and staging leads to scope extrusion, a form of typeunsoundness. For example, evaluating the expression
let r = ref .<1>. in.<fun y -> .~(r := .<y>.; .<()>.)>.;!rin MetaOCaml yields .<y_1>., a code fragment that contains an
unbound variable and is thus ill-formed. Mutation and other ef-

fects such as exceptions and control defeat MetaOCaml’s guaranteethat the generated code is well-formed and well-typed. Therefore,
MetaOCaml does not assure that y_memo_m is safe to use, eventhough in this case it is.
The most profitable optimizations in each domain often involvea different set of combinators—for memoizing results, pivoting
matrices, simplifying arithmetic, and so on (Cohen et al. 2006).
Therefore, a language for code generation should empower notjust a programming-language researcher but also an application
programmer to create combinator libraries, including those using
mutation. For such wide use of side effects, the language should
assure type soundness, especially the absence of scope extrusion.
2.2

Let-insertion

Besides the risk of scope extrusion, there is a second, deeper problem: code duplication. Suppose we stage gib with open recursion:
let sgib x y self n =if n = 0 then x else
if n = 1 then y else.<.~(self (n-1)) + .~(self (n-2))>.
Now .<fun x y -> .~(y_memo_m (sgib .<x>. .<y>.) 5)>.
produces the same inefficient specialized gib as before, with thecomputation y_2 + x_1 repeated thrice. Whereas code generation is memoized, the generated code does not memoize (Bondorf and Danvy 1991). For example, we want y_memo_m (sgib.<x>. .<y>.) 4 to return .<let t = y + x in let u = t+ y in u + t>., where no computation is duplicated. In thisdesired output, self 2 should contribute the binding and use
of u, and self 3 those of t, but these contributions are not codefragments—subexpressions—that can be spliced in by escapes.
One way to insert let as desired is to write the code generator
in CPS or monadic style (Bondorf 1992; Danvy and Filinski 1990,
1992; Swadi et al. 2006). The memoized calls to the code generator
can then share the memoization table and insert let-bindings asnecessary, without risking scope extrusion. In monadic style, thefunction gib takes the following form (Swadi et al. 2005).
let sgib_c x y self n =if n = 0 then ret x else
if n = 1 then ret y elsebind (self (n-2)) (fun r1 ->bind (self (n-1)) (fun r2 ->ret .<.~r2 + .~r1>.))
We omit the definitions of the monad operations ret and bind andof the memoizing combinator that applies to sgib_c. All this code
no longer resembles textbook algorithms, so it has lost its appealof simplicity. Syntactic sugar for monadic code (Carette and Kiselyov 2008; Peyton Jones 2003; Wadler 1992) reduces the clutter
but not the need to name intermediate results such as r1 and r2
above. In practice (for example, to generate Gaussian-eliminationcode), monadic style imposes a severe notational overhead (Caretteand Kiselyov 2008) that alienates application programmers and obstructs our quest to help end users specialize their code.
2.3

If-insertion

We have seen that let-insertion is necessary to avoid code duplication in practical code generators and requires the unappealing useof CPS or monadic style. A similar pattern is if-insertion (or assertion insertion), illustrated below. The code generator gen invokes
an auxiliary generator retrieve to extract the result of a complex
computation on a working array.
let gen retrieve =.<fun array n -> (complex computation on array);.~(retrieve .<array>. .<n>.)>.

The auxiliary generator retrieve receives two code values fromgen, which represent an array and an index into it. The code
generated by retrieve could just read the n-th element of array.
let retrieve array n = .< (.~array) . (.~n) >.
We would like, however, to check that n is in the bounds of array.
We could insert the bounds check right before the array access:let retrieve array n =.<assert (.~n >= 0 && .~n < Array.length .~array);(.~array) . (.~n)>.
Such a check is too late: we want the check right after the arrayand the index are determined, before any complex computationscommence. We wish the generator gen to yield.<fun array_1 -> fun n_2 ->assert (n_2 >= 0 && n_2 < Array.length array_1);(complex computation on array_1);
array_1.(n_2)>.
Again it seems impossible for retrieve to splice in the assert
far from the escape in gen. Again this difficulty can be overcome
by writing generators in CPS or monadic style, which looks foreign
to the application programmer.
2.4

Delimited control and its risk of scope extrusion

Lawall and Danvy (1994) show how to use Danvy and Filinski’s
delimited control operators shift and reset (1989, 1990, 1992)
to perform let- and if-insertion in the familiar direct style, by effectively hiding trivial uses of continuations as in sgib_c above. Sincedelimited control operators are available in MetaOCaml (Kiselyov2006), we can build a memoizing staged fixpoint combinator y_ms
with this technique, so that evaluating.<fun x y -> .~(top_fn (fun _ ->y_ms (sgib .<x>. .<y>.) 5))>.
—using the same direct-style sgib in §2.2—gives the ideal code.<fun x_1 -> fun y_2 ->let z_3 = y_2 in
let z_4 = x_1 in
let z_5 = (z_3 + z_4) in
let z_6 = (z_5 + z_3) in
let z_7 = (z_6 + z_5) in (z_7 + z_6)>.
without duplicating computations. (We describe y_ms and top_fn
in §3.4.) The same delimited control operators let us accomplish
if-insertion using the intuitive version of gen in §2.3.
Delimited control, however, is a side effect whose unrestricted
use poses the risk of scope extrusion. For example, the expression
top_fn (fun _ -> .<fun x y -> .~(y_ms (sgib .<x>. .<y>.) 5)>.)is well-typed in MetaOCaml with shift and reset added, but it
evaluates to the following code value, which disturbingly uses thevariables y_2 and x_1 unbound.
.<let z_3 = y_2 in
let z_4 = x_1 in
let z_5 = (z_3 + z_4) in
let z_6 = (z_5 + z_3) in
let z_7 = (z_6 + z_5) in
fun x_1 -> fun y_2 -> (z_7 + z_6)>.

3.

Combining staging and control safely

To eliminate the risk of scope extrusion just demonstrated, we propose a simple restriction: informally, we place an implicit presentstage reset under each future-stage binder. Any escape under aVariables
Expressions

x, y, z, f , k, n
e ::= i | e + e | λ x. e | fix | ee | (e, e) | fst | snd| ifz e then e else e | 出 | {e} | <e> | ∼e | x
Figure 1. Syntax of λ1

Valuesv0 ::= i | λ x. e | fix | (v0 , v0 ) | fst | snd | 出 | <v1 > | x
v1 ::= i | v1 + v1 | λ x. v1 | fix | v1 v1 | (v1 , v1 )| fst | snd | ifz v1 then v1 else v1 | 出 | {v1 } | x

Frames

F 0 ::=  + e | v0 +  | e | v0  | (, e) | (v0 , )| ifz  then e else e
F 1 ::=  + e | v1 +  | e | v1  | (, e) | (v1 , )| ifz  then e else e | ifz v1 then  else e| ifz v1 then v1 else  | {}Delimited contexts
D00 ::=  | D00 [F 0 ] | D01 [∼]
D10 ::= D10 [F 0 ] | D11 [∼]
D01 ::= D01 [F 1 ] | D00 [<>]
D11 ::=  | D11 [F 1 ] | D10 [<>]Contexts C0 ::= D00 | C0 [{D00 }] | C1 [λ x. D10 ]C1 ::= D01 | C0 [{D01 }] | C1 [λ x. D11 ]Figure 2. Values and contexts
future-stage binder thus incurs no effect observable outside thebinder’s scope. This restriction turns out not to preclude memoization, let-insertion, and if-insertion—which application programmers can now implement safely (without scope extrusion) and naturally (in direct style).
In this section, we detail our proposal by introducing a languagewith staging and control effects that builds in this restriction and,as we prove, prevents scope extrusion. Our language λ1 models asubset of MetaOCaml extended with delimited control operators.
Figure 1 shows the syntax: it features integer literals i and theirarithmetic +, λ -abstractions and their applications, pairs (e1 , e2 )and their projections fst and snd. We write let x = e1 in e2 as shorthand for (λ x. e2 )e1 . The conditional ifz e then e1 else e2 reduces to
e1 if e is zero, and to e2 otherwise. The constant fix is the applicative fixpoint combinator. As usual, we identify α-equivalent terms
and assume Barendregt’s variable convention. The operational semantics of these constructs is standard and call-by-value, as definedin Figures 2 and 3 in terms of small steps
and evaluation contexts C0 . In the subsections below, we explain the staging forms <e>and ∼e, the level superscripts 0 and 1, the delimited control forms
出 and {e}, and their interaction and typing.
We have implemented the language in Twelf, where the efficient Gibonacci generator can run. Unlike our Twelf implementation, MetaOCaml does not currently build in our restriction, so wemust manually examine each escape under a future-stage binderand check that it has no observable control effect. It is possible
to automate this check, either by extending MetaOCaml’s typechecker or by building a separate tool like Leroy and Pessaux’s
exception checker (2000).
3.1

Staging

As described in §2, our staging facility is comprised of brackets<e> and escapes ∼e. The staging level of an expression affects
whether it is a value and how a non-value is decomposed into a
C0 i1 + i2C0 (λ x. e) v0
C0 fix v0
C0 fst (v01 , v02 )
C0 snd (v01 , v02 )
C0 ifz 0 then e1 else e2
C0 ifz i then e1 else e2
C0 {v0 }

C1 ∼<v1 >
C0 {D00 [出v0 ]}C1 λ x. D10 [出v0 ]
C0 i1 +̇ i2C0 e[x := v0 ]
C0 λ x. v0 (fix v0 )x
C0 v01 
C0 v02


C0 e1
 
C0 e2
if i 6= 0
 0
0
C v
 
C1 v1


C0 {v0 (λ x. {D00 [x]})}
C1 λ x. ∼{<D10 [出v0 ]>}Figure 3. Operational semantics: small-step reduction e

(+)
(βv )

({})
(∼)
(出0 )
(出1 )
e0

context and a redex (Taha 2000). Our calculus has only two levels,present-stage and future-stage.2 They correspond to two evaluation‘modes’, reduction and code-building. To notate these levels, we
put the superscripts 0 and 1 on metavariables, such as values andcontexts in Figure 2.3 Brackets enclose a present-stage expression
to form a future-stage expression, whereas escapes do the opposite.
In particular, present-stage values v0 include code fragments <v1 >,which are bracketed expressions containing no escapes.
A present-stage context C0 can be plugged (that is, have its
hole  replaced) with a present-stage expression e to form a complete program C0 [e], whereas a future-stage context C1 can beplugged with a future-stage expression. As is usual in a multilevel
language, these contexts may contain future-stage bindings introduced by λ , so present-stage evaluation can occur in the body ofa future-stage abstraction. Contexts Ci are defined by composing
delimited contexts Di j , which can be plugged with a level- j expression to form a level-i expression. Delimited contexts are in turn defined by composing frames F i , which can be plugged with a level-i
expression to form a slightly larger level-i expression. In a degenerate language with neither staging nor delimited control, the superscripts would all be 0, and a context C0 and a delimited context D00
would both be just a sequence of frames F 0 .
If for a moment we disregard delimited control operators (to be
explained in §3.2), then the language λ1 is almost the same as ourα (Kameyama et al. 2008), butearlier two-level staged calculus λ1v
without cross-stage persistence (CSP) and without the operation
run to execute generated code. It can thus be regarded as Davies’s
λ (1996) restricted to two levels. It is also similar to Nielson andNielson’s (1988, 1992) and Gomard and Jones’s (1991) two-level
λ -calculi (though the latter does not type-check generated code).
Excluding run from our language makes it simpler to implement (because the run-time system need not include a compiler anddynamic linker) and to prove sound (because the type system need
not include environment classifiers (Taha and Nielsen 2003) to prevent attempts to run open code). The inability to run generated
code in the language may appear severe, but it is no different fromthe inability of the typical compiler (especially cross-compiler) toload and run any generated code in the compiler process itself. A
code generator written in λ1 cannot run any generated code on the
fly to test it, but the generated code is guaranteed to be well-typed
and can be saved to a source file to be compiled and run in a separate process. That is enough for the intended use for λ1 , namely
2 More levels would clutter the notation but are probably not hard to add.
3 Our Twelf formalization marks each expression as well with its level, but

we suppress those superscripts in this paper.

implementing DSL ‘compilers’ that generate families of optimized
library routines—such as Gaussian elimination (Carette and Kiselyov 2008), Fast Fourier Transform (Frigo and Johnson 2005; Kiselyov and Taha 2005), linear signal processing (Püschel et al. 2005),
and embedded code (Hammond and Michaelson 2003)—to be used
in applications other than the generator itself.
The lack of CSP in λ1 means that there is no ‘lift’ operation
to uniformly convert a present-stage value of any type to somefuture-stage code that evaluates to that value. However, λ1 can
express lifting at specific data types—integers, pairs of integers,
and such. Whereas CSP is important when using run (Taha andNielsen 2003), it is unnecessary for mere code generation. It caneven be harmful if unrestricted, because a generated library routine
ought to be usable without the generator present.
3.2

Delimited control

Delimited control is realized by the control delimiter { } (pronounced ‘reset’) and the constant 出 (pronounced ‘shift’).
When 出 is not used, the expression {e} (pronounced ‘reset e’)is evaluated like e, as if {e} were just shorthand for (λ x. x)e. We
specify this behavior by allowing contexts C0 to include resets { }.
The constant 出 is supposed to be applied to a function value,
say v0 . When 出v0 is evaluated, it captures the part of the current
evaluation context C0 up to the nearest dynamically enclosing delimiter. We call this part a delimited context D00 ; unlike C0 , it does
not include reset. As the 出0 rule in Figure 3 shows, the subexpression D00 [出v0 ] reduces to the application v0 (λ x. {D00 [x]}), reifying
the captured delimited context D00 as the abstraction λ x. {D00 [x]}.
We illustrate delimited control by using it to simulate mutablestate (Filinski 1994; Kiselyov et al. 2006). We define the terms
const = λ y.λ z.y, get = 出(λ k.λ z.kzz), put = λ z0 .出(λ k.λ z.kz0 z0 ).
The reduction sequence below illustrates how const and get work.
{const (get + 40)} 2

出0 {(λ k. λ z. kzz)(λ x. {const(x + 40)})} 2{λ z. (λ x. {const(x + 40)})zz} 2{} (λ z. (λ x. {const(x + 40)})zz) 2βv (λ x. {const(x + 40)}) 2 2
βv {const(2 + 40)} 2

βv

The first step replaces get and its delimited context const( + 40)
by an application of λ k. λ z. kzz to the function λ x. {const(x + 40)}.
The latter function is precisely the captured delimited context,
enclosed in reset and reified as a function. This single step can be
decomposed into a sequence of finer-grain reductions in which the
出-application bubbles up and builds up the delimited context bylocal rewriting (Felleisen and Friedman 1987; Parigot 1992).
Comparing the initial and final programs in this reduction sequence shows that its net result is to replace the expression getwith 2. It is as if the number 2 were stored in a cell and accessedby get in the program get + 40. The reductions continue to a value.
{const 42} 2βv {λ z. 42} 2{} (λ z. 42) 2βv 42

We can mutate the state: the term put(get + 1) increments thenumber in the cell and returns the new number.
{const (put(get + 1) + get)} 2 + {const (put(2 + 1) + get)} 2+ {const (put 3 + get)} 2+ (λ x. {const (x + get)}) 3 3
βv {const (3 + get)} 3
This sequence of reductions replaces the term put(get + 1) with 3
and at the same time puts the new value 3 outside the reset. The
result reduces to {const(3 + 3)} 3 and eventually 6. In general, theterm {const e}v0 behaves as if the expression e were executed inthe ‘context’ of a mutable cell initialized to v0 . Inside e, occurrences of get retrieve the current value of the cell, and a subterm of
the form 出(λ k. λ z. kz0 z0 ) assigns z0 to the cell.
Although our language has no mutable state, we have just emulated it using delimited control. We can therefore treat a memoization table as a piece of mutable state, express the memoizing fixpoint combinator y_memo_m (see the accompanying code incircle-shift.elf), and use it to transparently memoize gib or
another dynamic-programming algorithm in λ1 .
For the purpose of code generation, emulating mutable state
by delimited control brings two benefits. First, our core calculus
is smaller and its soundness is simpler to prove. Second, the delimited nature of our control operations lets us limit the lifetime(or dynamic extent (Moreau 1998)) of the mutable state. In otherwords, we can make sure that a mutable cell is only accessed or
updated during the evaluation of a particular subexpression. To prevent scope extrusion, it is crucial that our language provide this assurance both in the operational semantics (described in §3.3 below)
and in the type system (described in §3.5 below). Although optimizing compilers of imperative languages can determine the extent
of mutation by control-flow analyses, the results of the analyses are
not expressed in the language or exposed to the programmer.
3.3

Staging and delimited control, without scope extrusion

At first glance, it appears straightforward to combine staging anddelimited control. For example, the emulation of mutable state bydelimited control appears to work as explained in §3.2 even if
we store code values rather than integers in the mutable state andaccess them within escapes. For example, the following example
reuses a code value using const, get, and put.
{const <∼(put<8 + 5>) + ∼get>} <0>{const <∼(出(λ k. λ z. k<8 + 5><8 + 5>)) + ∼get>} <0>
出0 {(λ k. λ z. k<8 + 5><8 + 5>)(λ x. {const<∼x + ∼get>})} <0>+ {const <∼<8 + 5> + ∼get>} <8 + 5>
+ <(8 + 5) + (8 + 5)>∼ {const <(8 + 5) + ∼get>} <8 + 5>βv

Like in §3.2, put<8 + 5> assigns <8 + 5> to the mutable cell, so getlater is replaced by <8 + 5>. The final result is a piece of generated
code that, when evaluated in the future stage, will add 5 to 8 twice.
The only apparent difference between this emulation of mutablestate and the examples in §3.2 is that captured delimited contexts,
such as λ x. {const<∼x + ∼get>} in the second reduction above,
may span across brackets and escapes.
We now confront the two problems described in §2 that arise
when memoizing code generators. The first problem is the risk ofscope extrusion, which can happen when we store a code value thatuses a bound variable then splice the code value outside the scopeof the variable. Let us try to trigger scope extrusion in λ1 :{const (let x = <λ y. ∼(put<y>)> in get)} <0>
If put<y> above were to assign the code value <y> to the mutable
cell and get were to retrieve that code value, then this program
would generate the ill-scoped code <y>. Fortunately, put cannot
reach the mutable cell because the future-stage binder λ y stands
in the way. In Figure 2, this restriction is built into the definitionof delimited contexts, which excludes not only present-stage resets
but also future-stage binders. Our attempt at scope extrusion thus
fails; in fact, the type system in §3.5 below rejects it statically. We
prove that scope extrusion is impossible in §4.
The 出1 rule in Figure 3 shows that a future-stage binder acts
as a control delimiter just as a present-stage reset does: a futurestage abstraction λ x. e implicitly expands to λ x. ∼{<e>}. In thisregard, staging and delimited control are not orthogonal: wheneverstaging brings evaluation under λ , any side effect (in particular thelifetime of mutable state) must also stay under λ . Our language
prevents different future-stage scopes from sharing a memoizationtable, because doing so risks scope extrusion.
The second problem with memoizing code, described in §2.2,
is that the generated code duplicates computations such as 8 + 5
above. Armed with delimited control operators, we can now solve
this problem by inserting let in the generated code without writing
our code generator in CPS or monadic style. To illustrate this key
idea (due to Lawall and Danvy (1994) in an untyped setting), we
define the following alternative to put.

y ms = λ f . f (fix (λ self . λ n.
let x = 出(λ k. λ table. k (lookup n table) table) in
ifz fst x
then let y = f self n in
出(λ k. λ table. <let z = ∼y in ∼(k<z>(ext table n <z>))>)
else {snd x 0}))

put0 = λ z0 . 出(λ k. λ z. <let x = ∼z0 in ∼(k<x><x>)>)(int , int → τ): the variant None is represented as (0, fix λ f . f ) andthe variant Some x as (1, λ z. x).
When y ms is applied to a user function f and that function
invokes self on an integer argument n, our combinator retrieves thecurrent state of the memoization table to check if code has been
generated for n already. The lookup result (a pair) is bound to thevariable x in Figure 4. If fst x is zero, meaning n is new, then the
combinator invokes f to generate an expression y for n, binds y toa new future-stage variable z, and updates the memoization table tomap n to <z>. If the lookup succeeds (the last line of the code), thecombinator returns the found value without invoking f .
In this way, we have successfully specialized the Gibonacci
function in direct style as well as Gaussian elimination and Swadi
et al.’s (2005) other examples. These successes show that our language is expressive enough for practical applications, despite notallowing delimited control to reach beyond any binder.
If-insertion is also within reach. To use a simpler example thanin §2.3, suppose that gen is a code generator in λ1 of the form
λ f . <λ n. e + ∼( f <n>)>, where e is some complex computation. The
argument f is an auxiliary generator, a function from code to code.
Suppose that the code produced by f only makes sense if the futurestage argument n is nonzero—perhaps f <n> computes the inverseof n. We would like the generated code to check if n is nonzero
before evaluating e. To achieve this goal, we can define f to be

Using this put0 instead of put, it is easy to insert let in the generated
code to avoid duplicating computations.
{const <∼(put0 <8 + 5>) + ∼get>} <0>{const <∼(出(λ k. λ z. <let x = ∼<8 + 5> in ∼(k<x><x>)>))+ ∼get>} <0>
{(λ
k.
λ
z.
<let x = ∼<8 + 5> in ∼(k<x><x>)>)0
出(λ x. {const<∼x + ∼get>})} <0>+ <let x = 8 + 5 in ∼({const <x + ∼get>} <x>)>+ <let x = 8 + 5 in x + x>βv

Instead of storing any code for reuse that may contain a complex
computation, put0 inserts a let to bind the result of the computation
to a new variable (x = 8 + 5 above) that takes scope over the entire
generated expression, then stores just the variable. The generated
code performs the computation only once and can reuse the result.
3.4

Payoff: safe and efficient code generation in direct style

We have shown how to simulate mutable state and perform letinsertion using delimited control. Using these techniques, we havebuilt the desired memoizing staged fixpoint combinator y ms (seecircle-shift.elf for the complete code and tests). Roughly,4y ms has the type ((int → <int>) → int → <int>) → int → <int>.
As this type suggests, this combinator should be applied to a code
generator with open recursion, whose first argument is the recursive
instance of itself, and whose second argument is a present-stage
integer on which to specialize and recur. For example, recall thesgib function of §2.2:
sgib = λ x. λ y. λ self . λ n. ifz n then x else
ifz n − 1 then y else<∼(self (n − 1)) + ∼(self (n − 2))>
To specialize the Gibonacci function to n = 5, we evaluate5<λ x. λ y. ∼({const (y ms (sgib <x><y>) 5)} empty)>(where empty is the empty memoization table) to obtain<λ x. λ y. let z3 = y in let z4 = x in let z5 = z3 + z4 in
let z6 = z5 + z3 in let z7 = z6 + z5 in z7 + z6 >.
This result is the ideal promised in §2.4—a linear sequence of
operations without any code duplication.
Figure 4 shows our definition of y ms. This fixpoint combinatorsimulates mutable state to maintain a memoization table that maps
integer keys to previously generated code values. Therefore, it uses
the table operations empty, lookup, and ext specified in §2.1,
which are trivial to implement. Whereas lookup in §2.1 returns
a value of type int option, our language λ1 does not include
option, so we emulate the sum type τ option by a product type
4 We suppress effect annotations in types until §3.5, where we introduce thetype system formally.
5 This example reveals that top fn in §2.4 is λ z. {const (z 0)} empty.

Figure 4. The memoizing staged fixpoint combinator y ms

λ n. 出(λ k. <ifz ∼n then fail else ∼(k<inverse ∼n>)>).
Passing this auxiliary generator to gen produces the desired code
<λ n. ifz n then fail else e + inverse n>.
The complex expression e will not be evaluated if n turns out zero.
3.5

Type system

Figure 5 displays the type system of our language λ1 . It combines
a simplification of Danvy and Filinski’s type system for delimited
control (1989) and a simplification of Davies’s type system forstaging (1996) in a sound but not orthogonal way.
The types τ of λ1 are the base type int, arrow types τ → τ 0 /τ0 ,product types (τ, τ 0 ), and code types <υ/υ0 >. The type system ismonomorphic like the simply-typed λ -calculus; we include typevariables α only to state that our language has principle typings.
Without impredicative effect polymorphism (Asai and Kameyama2007), in order to write the desired code as in §3.4, we are forced
to build product types into the language rather than Church-encode
them. (This task is not difficult; sum types would have sufficed too.)
As a two-level language, λ1 operates on code values in thepresent stage only. Hence, we require the types of future-stage
expressions to be flat, that is, to contain no code types. Types
with nested brackets such as <<int / int>/ int> are thus excluded
along with terms such as <<42>>. A type environment Γ is a set of
associations x : τ of present-stage variables x with general types τand associations <x : υ> of future-stage variables x with flat types υ.
There are two judgment forms, one that assigns general types topresent-stage expressions and one that assigns flat types to futurestage expressions. Both forms include answer types to track thecontrol effects that may occur: in a present judgment Γ ` e : τ ; τ0 ,

Type variables
Flat type variables

Types
Flat types
Environmentsαβτ ::= int | τ → τ 0 /τ0 | <υ/υ0 > | (τ, τ 0 ) | αυ ::= int | υ → υ 0 /υ0 | (υ, υ 0 ) | βΓ ::= [] | Γ, x : τ | Γ, <x : υ>Γ, x : τ ` e : τ 0 ; τ1

Γ ` e1 : int ; τ0 [; υ0 ] Γ ` e2 : int ; τ0 [; υ0 ]
Γ ` i : int ; τ0 [; υ0 ]

Γ ` (λ x. e) : τ → τ /τ1 ; τ0

Γ ` e1 : τ → τ 0 /τ0 ; τ0

Γ ` e2 : τ ; τ0

Γ ` (λ x. e) : υ → υ 0 /υ1 ; τ0 ; υ0

Γ ` e1 : υ → υ 0 /υ0 ; τ0 ; υ00

Γ ` fix : (T → T /τ2 ) → T /τ1 ; τ0 [; υ0 ]

Γ ` e : τ ; τ0
Γ ` e : υ ; τ0 ; υ0Γ, <x : υ> ` e : υ 0 ; <υ 0 /υ1 > ; υ10

Γ ` e1 + e2 : int ; τ0 [; υ0 ]T = (τ → τ 0 /τ2 )Present judgments
Future judgmentsΓ ` e2 : υ ; τ0 ; υ0

Γ ` e1 e2 : υ 0 ; τ0 ; υ0

Γ ` e1 e2 : τ ; τ0

Γ ` e : τ ; τ0 [; υ0 ] Γ ` e0 : τ 0 ; τ0 [; υ0 ]
Γ ` (e, e0 ) : (τ, τ 0 ) ; τ0 [; υ0 ]

Γ ` fst : (τ, τ 0 ) → τ/τ1 ; τ0 [; υ0 ]

Γ ` snd : (τ, τ 0 ) → τ 0 /τ1 ; τ0 [; υ0 ]

Γ ` e : int ; τ0 [; υ0 ] Γ ` e1 : τ ; τ0 [; υ0 ] Γ ` e2 : τ ; τ0 [; υ0 ]
Γ ` 出 : ((τ → τ 0 /τ1 ) → τ 0 /τ 0 ) → τ/τ 0 ; τ0 [; υ0 ]

Γ ` ifz e then e1 else e2 : τ ; τ0 [; υ0 ]
Γ`e:τ ;τΓ ` e : υ ; τ0 ; υΓ ` e : υ ; τ 0 ; υ0

Γ ` e : <υ/υ0 > ; τ0(x : τ) ∈ Γ(<x : υ>) ∈ ΓΓ ` {e} : τ ; τ0

Γ ` {e} : υ ; τ0 ; υ0

Γ ` <e> : <υ/υ0 > ; τ0

Γ ` ∼e : υ ; τ0 ; υ0

Γ ` x : τ ; τ0

Γ ` x : υ ; τ0 ; υ0Figure 5. The type system of λ1
the answer type is τ0 at the present stage; in a future judgmentΓ ` e : υ ; τ0 ; υ0 , the answer types are τ0 at the present stageand υ0 at the future stage.6 The future answer type υ0 is needed
to ensure that the generated code, which may incur control effects
in the future stage, never goes wrong. Those type metavariables
in Figure 5 with numeric subscripts (such as τ0 ) are answer types
that can be ignored on the first reading. Because constructs such asaddition that have nothing to do with staging or delimited control
are type-checked in the same way at both stages, we write Γ ` e :τ ; τ0 [; υ0 ] to mean either a present judgment (without ‘; υ0 ’) or afuture judgment (with ‘; υ0 ’ and requiring τ to be flat).
An answer type is the type of the result of plugging an expression into a delimited context. In other words, an answer type is thetype of an expression surrounded by a control delimiter. To take an
example from §3.2, in the program {const (get + 40)} 2, the answer type of the expression get plugged into the delimited context
const( + 40) is the type of a function from int to int, even though
the whole program has the type int instead. In terms of CPS, ananswer type is just the codomain type of a continuation or computation. In fact, our type system is just a ‘pullback’ of the staged typesystem of our CPS target language in §5.
Because answer types are effect annotations, they appear notjust in judgments but also in function types and code types (‘/τ0 ’
and ‘/υ0 ’), where effects are delayed. The typing rules for λ x. eshow that the effect of e (represented by the answer types τ1 and υ1 )is incurred only when the function is invoked. The typing rules for<e> and ∼e show that the future effect of a code value (represented
by the answer type υ0 ) will be incurred only where the code valueis spliced in (and never in the present stage).
An expression is pure if it incurs no observable control effect;a pure expression is polymorphic in its answer type(s) (Thielecke2003). For example, it is easy to derive the judgment Γ ` (2 + 40) :int ; τ0 for an arbitrary answer type τ0 . In words, it is safe to plug
the expression 2 + 40 into any delimited context that expects an int,
no matter what type τ0 results from the plugging. In contrast, theexpression get + 40 incurs a control effect, as observed in §3.2.
Our type system detects this effect: it derives the judgment Γ `(get + 40) : int ; τ0 if and only if the answer type τ0 has the form
int → τ 0 /τ1 . In words, it is safe to plug the expression get + 40
into a delimited context that expects an int if and only if a function
from int results from the plugging.
6 For simplicity, we equate the two answer types distinguished by Danvy

and Filinski (1989). The distinction is not hard to add, but not needed here.

All values are pure. Control delimiters also make an expressionpure, by masking its effect: in the typing rules for present-stage {e}and future-stage λ x. e, the answer type τ0 is arbitrary. The latter
rule crucially forces future-stage binders to delimit present-stage
control: the present-stage answer type is the code type <υ 0 /υ1 > inthe premise but arbitrary in the conclusion.
As an example, the following derivation shows that the program{const (get + 40)} 2 in §3.2 is well-typed. (Let T = int → int /τ0
and S = ((int → T /τ0 ) → T /T ) → int /T .)..
..
k : (int → T /τ0 ) ` λ z. kzz : T ; T[] ` 出 : S ; T [] ` λ k. λ z. kzz : (int → T /τ0 ) → T /T ; T[] ` get : int ; T[] ` get + 40 : int ; T[] ` const (get + 40) : T ; T[] ` {const (get + 40)} : T ; τ0[] ` {const (get + 40)} 2 : int ; τ0
The accompanying file circle-shift.elf type-checks many
tests in Twelf. For example, the fixpoint combinator y ms in §3.3
has the type ((int → <υ/υ1 >) → int → <υ/υ0 >) → int → <υ/υ0 >,in which the present-stage answer types are all (int → T /T ) →<υ 0 /υ0 >/<υ 0 /υ0 >, in which int → T /T is the type of the memoization table, and the type T = (int , int → <υ/υ0 >/<υ/υ0 >) encodes
the lookup result type <υ/υ0 > option as explained in §3.4.

4.

Formal properties

Proposition 4.1 (principal typing) If e is a term such that some
judgment Γ ` e : τ ; τ0 [; υ0 ] is derivable, then some judgmentΓ ` e : τ ; τ0 [; υ0 ] is derivable such that, for any derivable judgment
Γ0 ` e : τ 0 ; τ00 [; υ00 ], there exists a substitution θ for type variables
and flat type variables so that Γ0 ⊇ Γθ , τ 0 = τθ , and τ00 = τ0 θ [and
υ00 = υ0 ].
Proof Our syntax-directed type system constitutes an algorithm
to infer Γ, τ, and τ0 [and υ0 ] from e using unification.
Proposition 4.2 (subject reduction) If Γ ` e : τ ; τ0 is derivableand e e0 , then Γ ` e0 : τ ; τ0 is derivable.
Proof We first note that, if Γ ` v0 : τ ; τ0 is derivable, thenΓ ` v0 : τ ; τ1 is derivable for any type τ1 . We need a substitution

lemma: if Γ, x : τ ` e : τ 0 ; τ0 [; υ0 ] and Γ ` v0 : τ ; τ1 [; υ1 ], thenΓ ` e[x := v0 ] : τ 0 ; τ0 [; υ0 ]. We also need a weakening lemma: if
Γ ` e : τ ; τ0 [; υ0 ], then Γ, ∆ ` e : τ ; τ0 [; υ0 ]. The proofs are routine.
Because our typing rules are all compositional, we can assume
without loss of generality that C0 and C1 in Figure 3 are just . We
prove the proposition by case analysis on the reduction. We show a
few interesting cases.
Case βv : Suppose Γ ` (λ x. e)v0 : τ 0 ; τ0 . By inversion, we haveΓ, x : τ ` e : τ 0 ; τ0 and Γ, v0 ` τ ; τ0 for some τ. Then the substitution
lemma gives Γ ` e[x := v0 ] : τ 0 ; τ0 .
Case 出0 : We have the derivation..
..
Γ ` 出 : T → τ/τ 0 ; τ 0 Γ ` v0 : T ; τ 0Γ ` 出v.0 : τ ; τ 0..
.

Γ ` D00 [出v0 ] : τ 0 ; τ 0
Γ ` {D00 [出v0 ]} : τ 0 ; τ0where T = (τ → τ 0 /τ1 ) → τ 0 /τ 0 and the derivation from 出v0 to
D00 [出v0 ] does not change the answer type τ 0 . Then we can use theweakening lemma to derive:
Γ, x : τ ` x : τ ; τ 0..
..

Γ, x : τ ` D00 [x] : τ 0 ; τ 0
Γ, x : τ ` {D00 [x]} : τ 0 ; τ1
Γ ` v0 : T ; τ 0Γ ` λ x. {D00 [x]} : τ → τ 0 /τ1 ; τ 0

Γ ` v0 (λ x. {D00 [x]}) : τ 0 ; τ 0
Γ ` {v0 (λ x. {D00 [x]})} : τ 0 ; τ0Case 出1 : Suppose Γ ` λ x. D10 [出v0 ] : υ → υ 0 /υ1 ; τ0 ; υ0 . By
inversion, Γ, <x : υ> ` D10 [出v0 ] : υ 0 ; <υ 0 /υ1 > ; υ1 . Then it is easy
to derive Γ ` λ x. ∼{<D10 [出v0 ]>} : υ → υ 0 /υ1 ; τ0 ; υ0 .
Corollary 4.3 (absence of scope extrusion) If [] ` e : τ ; τ0 isderivable and e ∗ e0 , then e0 does not contain free variables.
By induction on the number of steps from e to e0 .

ProofTo state the next two propositions, we define the type environment <Γ> = <x1 : υ1 >, . . . , <xn : υn > whenever Γ = x1 : υ1 , . . . , xn : υn .
Proposition 4.4 (progress) If <Γ> ` {e} : τ ; τ0 is derivable thenthere exists a term e0 such that {e} e0 .
Proof By induction on the derivation of <Γ> ` {e} : τ ; τ0 .
The statement of this proposition differs from the ordinary form in
two respects. First, we consider terms in the form {e} only, sincea term like 出v0 by itself, without an enclosing control delimiter,cannot be reduced. Second, we allow a potentially non-empty environment <Γ>, in order for the inductive proof to go through.
Propositions 4.2 and 4.4 together show that well-typed programs never go wrong in λ1 . In particular, well-typed code generators never go wrong. Moreover, any code they generate never goes
wrong either, by the following argument. If [] ` {e} : <υ/υ0 > ; τ0 isderivable, then the program {e} either fails to terminate or evaluates
to a code value <v1 > such that [] ` v1 : υ ; τ0 ; υ0 . The next proposition then assures us that v1 is well-typed at the present stage.
Proposition 4.5 If <Γ> ` v1 : υ ; τ0 ; υ0 , then Γ ` v1 : υ ; υ0 .
Proof

By induction on the derivation of <Γ> ` v1 : υ ; τ0 ; υ0 . 

5.

CPS translation

We define a CPS translation for λ1 . Its target is λ1 without
present-stage control effects. In other words, the terms of the target
are as in λ1 but without the control operators 出 and { } at thepresent stage. The type system of the target is as in λ1 but withall present-stage answer types removed from types and judgments.
We define term equality in the target language as the least congruence containing all λ1 reductions (except {}, 出0 , 出1 ) and thecall-by-value η-reduction λ x. ex = e, even under present-stage λ .
First, we CPS-translate present-stage types τ to τ ∗ .
int∗ = int<υ1 /υ2 >∗ = <υ1 /υ2 >(τ1 , τ2 )∗ = (τ1∗ , τ2∗ )(τ1 → τ2 /τ3 )∗ = τ1∗ → (τ2∗ → τ3∗ ) → τ3∗α∗ = α(Future-stage types do not change.) We also translate environments.
[]∗ = []

(Γ, x : τ)∗ = Γ∗ , x : τ ∗(Γ, <x : υ>)∗ = Γ∗ , <x : υ>

The translation of terms depends on the level: a level-i term etranslates to JeKi for i = 0, 1; a level-0 value v0 translates to Lv0 M.
Jv0 K0 = λ k. kLv0 M

Je1 + e2 K0 = λ k. Je1 K0 (λ x. Je2 K0 (λ y. k(x + y)))Je1 e2 K0 = λ k. Je1 K0 (λ f . Je2 K0 (λ x. f xk))

J(e1 , e2 )K0 = λ k. Je1 K0 (λ x. Je2 K0 (λ y. k(x, y)))Jifz e then e1 else e2 K0 = λ k. JeK0 (λ x.
ifz x then Je1 K0 k else Je2 K0 k)
J{e}K0 = λ k. k(JeK0 (λ z. z))

J<e>K0 = JeK1
Lλ x. eM = λ x. JeK0

LfixM = λ y. λ k. k(fix (λ f . λ x. λ k0 . y f (λ z. zxk0 )))L(v01 , v02 )M = (Lv01 M, Lv02 M)

LpM = λ x. λ k. k(px) where p = fst, snd

L出M = λ f . λ k. f (λ x. λ k0 . k0 (kx))(λ z. z)
Lv0 M = v0 for all other values v0

Jv1 K1 = λ k. k <v1 >Je ⊕ e0 K1 = λ k. JeK1 (λ x. Je0 K1 (λ y. k <∼x ⊕ ∼y>))where e ⊕ e0 is e + e0 , ee0 , or (e, e0 )Jλ x. eK1 = λ k. k <λ x. ∼(JeK1 (λ z. z))>Jifz e then e1 else e2 K1 = λ k. JeK1 (λ x. Je1 K1 (λ y. Je2 K1 (λ z.
k <ifz ∼x then ∼y else ∼z>)))J{e}K1 = λ k. JeK1 (λ x. k <{∼x}>)J∼eK1 = JeK0

The output of the translation is in tail form except in J{e}K0 ,L出M, and Jλ x. eK1 . If we define Jλ x. eK1 = λ k. JeK1 (λ z. k <λ x. ∼z>)naively in tail form, then occurrences of x in e would translate tounbound future-stage variables. The CPS translation thus relies on
our treating future-stage binders as present-stage control delimiters.
Proposition 5.1 (type preservation) If the present judgment Γ `e : τ ; τ0 is derivable in λ1 , then the present judgment Γ∗ ` JeK0 :(τ ∗ → τ0∗ ) → τ0∗ is derivable. If the future judgment Γ ` e : υ ;τ0 ; υ0 is derivable in λ1 , then the present judgment Γ∗ ` JeK1 :(<υ/υ0 > → τ0∗ ) → τ0∗ is derivable.
Proof By mutual induction on typing derivations.
For the level-0 translation, the only interesting case is whene = <e0 >. Suppose Γ ` e0 : υ ; τ0 ; υ0 . By the induction hypothesis,
we have Γ∗ ` J<e0 >K0 = Je0 K1 : (<υ/υ0 > → τ0∗ ) → τ0∗ .

For the level-1 translation, the interesting cases are as follows.
(Case e = x) Suppose Γ ` x : υ ; τ0 ; υ0 . Then (<x : υ>) ∈ Γ, so(<x : υ>) ∈ Γ∗ . Thus, Γ∗ ` JxK1 = λ k. k<x> : (<υ/υ0 > → τ0∗ ) → τ0∗ .
(Case e = λ x. e0 ) Suppose Γ, <x : υ 00 > ` e0 : υ 0 ; <υ 0 /υ1 > ; υ1 .
The induction hypothesis gives Γ∗ , <x : υ 00 > ` Je0 K1 : (<υ 0 /υ1 > →<υ 0 /υ1 >) → <υ 0 /υ1 >. Then Γ ` JeK1 = λ k. k <λ x. ∼(Je0 K1 (λ z. z))> :(<(υ 00 → υ 0 /υ1 )/υ0 > → τ0∗ ) → τ0∗ .
(Case e = {e0 }) Suppose Γ ` e0 : υ ; τ0 ; υ. By the induction
hypothesis, we have Γ∗ ` Je0 K1 : (<υ/υ> → τ0∗ ) → τ0∗ . Moreover,
we have Γ∗ , x : <υ/υ> ` <{∼x}> : <υ/υ0 >. Hence, we can deriveΓ∗ ` J{e0 }K1 = λ k. Je0 K1 (λ x. k <{∼x}>) : (<υ/υ0 > → τ0∗ ) → τ0∗ . 
Proposition 5.2 (equality preservation) If Γ ` e : τ ; τ0 is derivable and e e0 , then JeK0 = Je0 K0 .
The proof of this proposition can be found in Appendix B.
We leave to future work to prove simulation: if Γ ` e : τ ; τ isderivable and τ ∗ = τ, then the λ1 programs {e} and JeK0 (λ z. z)either both evaluate to the same value or both fail to terminate.

6.

Related work

Our work draws from two strands of research on partial evaluationand code generation, namely side effects and custom generators.
There is a long tradition of using CPS to write program generators such as pattern-match compilers. Danvy and Filinski (1990,
1992) first applied delimited control to program generation: they
showed how to fuse a CPS translation and administrative reductions into one pass by writing the translation either in CPS or using
shift and reset. Similarly in partial-evaluation research, Bondorf (1992) showed how to improve binding times by writing thespecializer rather than source programs in CPS. This move helps
because the specializer is a fixed program that a programming-language expert can write and prove correct once and for all, whereas
many source programs are written and fed to the specializer overtime, by domain experts who may be unfamiliar with CPS.
Danvy and Filinski’s CPS translations and Bondorf’s specializer
are sound, in the sense that their continuations are well-behaved
and do not lead to scope extrusion. Given that these code generators
were fixed, it was sensible for their authors to prove their soundness as part of specific proofs of their correctness, rather than asa corollary of some type system that assures that every well-typed
generator is sound. Lawall and Danvy (1994) did not rely on sucha type system either when they used shift and reset to reduce
Bondorf’s specializer to direct style. Our type system accepts thesegenerators not as is but reformulated as combinators (Thiemann1999). It thus assures them sound; in particular, it is the first to
accept Danvy and Filinski’s and Lawall and Danvy’s uses of delimited control. In contrast, we are not aware of any sound type systemfor code generators that accepts Sumii and Kobayashi’s specializer(2001), which performs let-insertion using mutable state rather thandelimited control to speed up specialization.
Programs in particular domains often need to be optimized or
specialized using specific techniques that experts of the domains
can implement more readily than compiler or specializer writers.
Examples include memoization for Gibonacci and dynamic programming (Swadi et al. 2006), pivoting for Gaussian elimination(Carette and Kiselyov 2008), and simplifying complex arithmetic
for Fast Fourier Transform (Frigo and Johnson 2005; Kiselyov andTaha 2005). To better support these domain-specific optimizations,
two approaches have been developed in the literature.
The first approach is to specialize a source language that has features (such as state) that help express custom optimizations. Alongthis line, Thiemann and Dussart (1999) built an offline specializer
for a higher-order language with mutable references. The example
source programs in their paper show how application programmers

can persuade their specializer to produce efficient code: by expressing unspecialized optimization techniques (such as memoization)and by improving binding times manually (for instance, writing arecursive coercion to transform static data into dynamic data).
As usual, Thiemann and Dussart’s specializer uses continuations to perform let-insertion. What is less usual is that it is written
in a store-passing style, so as to manage mutable references at specialization time. These static references are organized by a bindingtime analysis (BTA) into regions (Talpin and Jouvelot 1992), which
limit the references’ lifetimes much as is rudimentarily achievedby the simulation of state by delimited control in §3. To prevent
scope extrusion, the BTA ensures that a static reference is used in
the scope of a dynamic binder only if the reference’s lifetime is local to the binder. This constraint is analogous to our restriction of
static effects (not just mutation) to the scope of dynamic binders.
Whereas Thiemann and Dussart’s specializer infers binding-time
annotations and performs let-insertion automatically and safely, ourtype system (akin to their constraints on annotations) ensures thesafety of code generators written by application programmers.
The last difference brings us to the second way to support
domain-specific optimizations: letting domain experts write code
generators. This approach has the advantage that the behavior ofa code generator on a static input tends to be more predictable
than the behavior of a specializer (especially its BTA) on a source
program. Swadi et al.’s (2006) and Carette and Kiselyov’s (2008)
uses of CPS and monadic style in domain-specific code generators
raise the need for a multilevel language to provide the convenienceof effects without the risk of scope extrusion. Such a language isneeded to ease the development and assure the safety of a variety
of domain-specific code generators, not just a fixed specializer.
This paper addresses this need, following two previous papers.
To prevent scope extrusion in a multilevel language with references, Calcagno et al. (2000) proposed to store only values ofclosed types in mutable cells. This (unimplemented) proposal is too
restrictive for our purposes, because we want to store future-stage
variables in memoization tables (as in our Gibonacci example).
We previously (Kameyama et al. 2008) introduced a typed twoα and translated it to System F. That translationlevel language λ1v
fails in the presence of effects (due to scope extrusion, manifest
as a lack of type coercions), yet it is more complex than our CPS
translation in §5 here. So far, then, it seems simpler to combine
staging and effects by translating effects rather than staging away.

7.

Conclusions

We have presented the first language for writing code generatorsthat provides delimited control operators while assuring staticallythat all generated code is well-formed. This language thus strikes
a balance between clarity and safety that helps application programmers implement domain-specific optimizations in practical,
reusable generators of specialized programs. The key idea that enables this balance is to restrict control effects to the scope of generated binders, that is, to treat generated binders as control delimiters.
As the examples illustrate, our language is expressive enoughin many practical settings we have encountered. Nevertheless, itwould be useful to find a sound way to relax our restriction oncontrol effects, so as to perform let- and if-insertion outside theclosest generated binder. We could then express loop-invariant code
motion and generate assertions to be checked as early as possible.
It might also help us simultaneously access multiple pieces of state
at different generated scopes, not just one piece as in §3.2.
Another good way to enrich our language is to add delimited
control to a richer language (like Taha and Nielsen’s (2003)) withmore than two levels (probably not hard), run, and CSP. Finally,
our language can be made much more comfortable to use by adding
polymorphism over effect annotations (Asai and Kameyama 2007).

Acknowledgments
We thank Kenichi Asai, Olivier Danvy, and Atsushi Igarashi for
helpful discussions, and the reviewers for their comments.

References
Asai, Kenichi, and Yukiyoshi Kameyama. 2007. Polymorphic
delimited continuations. In APLAS, 239–254. LNCS 4807.
Bondorf, Anders. 1992. Improving binding times without explicit
CPS-conversion. In Lisp & functional programming, 1–10.
Bondorf, Anders, and Olivier Danvy. 1991. Automatic autoprojection of recursive equations with global variables and abstract
data types. Science of Computer Programming 16(2):151–195.
Calcagno, Cristiano, Eugenio Moggi, and Walid Taha. 2000.
Closed types as a simple approach to safe imperative multi-stage
programming. In ICALP, 25–36. LNCS 1853.
Carette, Jacques, and Oleg Kiselyov. 2008. Multi-stage programming with functors and monads: Eliminating abstraction overhead from generic code. Science of Computer Programming.
Cohen, Albert, Sébastien Donadio, Marı́a Jesús Garzarán,
Christoph Armin Herrmann, Oleg Kiselyov, and David A.
Padua. 2006. In search of a program generator to implement
generic transformations for high-performance computing. Science of Computer Programming 62(1):25–46.
Czarnecki, Krzysztof, John T. O’Donnell, Jörg Striegnitz, andWalid Taha. 2004. DSL implementation in MetaOCaml, Template Haskell, and C++. In DSPG 2003, 51–72. LNCS 3016.
Danvy, Olivier, and Andrzej Filinski. 1989. A functional abstraction of typed contexts. Tech. Rep. 89/12, DIKU, University of
Copenhagen, Denmark. http://www.daimi.au.dk/~danvy/
Papers/fatc.ps.gz.
———. 1990. Abstracting control. In Lisp & functional programming, 151–160.
———. 1992. Representing control: A study of the CPS transformation. Mathematical Structures in Computer Science 2(4):361–391.
Davies, Rowan. 1996. A temporal logic approach to binding-time
analysis. In LICS, 184–195.
Eckhardt, Jason, Roumen Kaiabachev, Emir Pašalić, Kedar N.
Swadi, and Walid Taha. 2005. Implicitly heterogeneous multistage programming. In GPCE, 275–292. LNCS 3676.
Elliott, Conal. 2004. Programming graphics processors functionally. In Haskell workshop, 45–56.
Felleisen, Matthias, and Daniel P. Friedman. 1987. A reduction semantics for imperative higher-order languages. In PARLE: Parallel architectures and languages Europe. Volume II: Parallellanguages, 206–223. LNCS 259.
Filinski, Andrzej. 1994. Representing monads. In POPL, 446–457.
Frigo, Matteo, and Steven G. Johnson. 2005. The design andimplementation of FFTW3. Proceedings of the IEEE 93(2):216–
231.
Gomard, Carsten K., and Neil D. Jones. 1991. A partial evaluator
for the untyped lambda calculus. Journal of Functional Programming 1(1):21–69.
Hammond, Kevin, and Greg Michaelson. 2003. Hume: A domainspecific language for real-time embedded systems. In GPCE,
37–56. LNCS 2830.
Kameyama, Yukiyoshi, Oleg Kiselyov, and Chung-chieh Shan.
2008. Closing the stage: From staged code to typed closures.
In PEPM, 147–157.
Kiselyov, Oleg. 2006.
Native delimited continuations in(byte-code) OCaml. http://okmij.org/ftp/Computation/
Continuations.html#caml-shift.
Kiselyov, Oleg, Chung-chieh Shan, and Amr Sabry. 2006. Delimited dynamic binding. In ICFP, 26–37.

Kiselyov, Oleg, and Walid Taha. 2005. Relating FFTW and splitradix. In ICESS, 488–493. LNCS 3605.
Lawall, Julia L., and Olivier Danvy. 1994. Continuation-based
partial evaluation. In Lisp & functional programming, 227–238.
Lengauer, Christian, and Walid Taha, eds. 2006. Special issue on
the 1st MetaOCaml workshop (2004), vol. 62(1) of Science ofComputer Programming.
Leroy, Xavier, and François Pessaux. 2000. Type-based analysis
of uncaught exceptions. ACM Transactions on Programming
Languages and Systems 22(2):340–377.
McAdam, Bruce J. 2001. Y in practical programs. Workshop on fixed points in computer science; http://www.dsi.
uniroma1.it/~labella/absMcAdam.ps.
MetaOCaml. 2006. MetaOCaml. http://www.metaocaml.org.
Michie, Donald. 1968. “Memo” functions and machine learning.
Nature 218:19–22.
Moreau, Luc. 1998. A syntactic theory of dynamic binding.
Higher-Order and Symbolic Computation 11(3):233–279.
Nielson, Flemming, and Hanne Riis Nielson. 1988. Automatic
binding time analysis for a typed λ -calculus. In POPL, 98–106.
———. 1992. Two-level functional languages. Cambridge University Press.
Parigot, Michel. 1992. λ µ-calculus: An algorithmic interpretationof classical natural deduction. In LPAR, 190–201. LNAI 624.
Pašalić, Emir, Walid Taha, and Tim Sheard. 2002. Tagless staged
interpreters for typed languages. In ICFP, 157–166.
Peyton Jones, Simon L. 2003. The Haskell 98 language and libraries. Journal of Functional Programming 13(1):1–255.
Püschel, Markus, José M. F. Moura, Jeremy Johnson, David
Padua, Manuela Veloso, Bryan W. Singer, Jianxin Xiong,Franz Franchetti, Aca Gačić, Yevgen Voronenko, Kang Chen,
Robert W. Johnson, and Nick Rizzolo. 2005. SPIRAL: Codegeneration for DSP transforms. Proceedings of the IEEE 93(2):232–275.
Sørensen, Morten Heine B., Robert Glück, and Neil D. Jones.
1994. Towards unifying deforestation, supercompilation, partial
evaluation, and generalized partial computation. In ESOP, 485–
500. LNCS 788.
Sumii, Eijiro, and Naoki Kobayashi. 2001. A hybrid approach toonline and offline partial evaluation. Higher-Order and Symbolic
Computation 14(2–3):101–142.
Swadi, Kedar, Walid Taha, and Oleg Kiselyov. 2005.
Dynamic programming benchmark. http://www.metaocaml.
org/examples/dp/.
Swadi, Kedar, Walid Taha, Oleg Kiselyov, and Emir Pašalić. 2006.
A monadic approach for avoiding code duplication when staging
memoized functions. In PEPM, 160–169.
Taha, Walid. 2000. A sound reduction semantics for untyped CBN
multi-stage computation. In PEPM, 34–43.
———. 2005. Resource-aware programming. In ICESS, 38–43.
LNCS 3605.
Taha, Walid, and Michael Florentin Nielsen. 2003. Environment
classifiers. In POPL, 26–37.
Talpin, Jean-Pierre, and Pierre Jouvelot. 1992. Polymorphic type,region and effect inference. Journal of Functional Programming
2(3):245–271.
Thielecke, Hayo. 2003. From control effects to typed continuationpassing. In POPL, 139–149.
Thiemann, Peter. 1999. Combinators for program generation. Journal of Functional Programming 9(5):483–525.
Thiemann, Peter, and Dirk Dussart. 1999. Partial evaluation forhigher-order languages with state. http://www.informatik.
uni-freiburg.de/~thiemann/papers/mlpe.ps.gz.
Wadler, Philip L. 1992. Comprehending monads. Mathematical
Structures in Computer Science 2(4):461–493.