A CPS-like Transformation of Continuation Marks

Kimball R. Germane

A thesis submitted to the faculty of
Brigham Young University
in partial fulfillment of the requirements for the degree ofMaster of Science

Jay McCarthy, Chair
Sean Warnick
Dennis Ng

Department of Computer Science
Brigham Young University
November 2012

Copyright c 2012 Kimball R. Germane
All Rights Reserved

ABSTRACTA CPS-like Transformation of Continuation Marks
Kimball R. Germane
Department of Computer Science, BYU
Master of Science
Continuation marks are a programming language feature which generalize stackinspection. Despite its usefulness, this feature has not been adopted by languages which relyon stack inspection, e.g., for dynamic security checks. One reason for this neglect may bethat continuation marks do not yet enjoy a transformation to the plain λ-calculus which
would allow higher-order languages to provide continuation marks at little cost.
We present a CPS-like transformation from the call-by-value λ-calculus augmented with
continuation marks to the pure call-by-value λ-calculus. We discuss how this transformation
simplifies the construction of compilers which treat continuation marks correctly. We document
an iterative, feedback-based approach using Redex. We accompany the transformation witha meaning-preservation theorem.

Keywords: continuation marks, continuation-passing style, Redex

ACKNOWLEDGMENTS

Thanks to Jay McCarthy for igniting a fire for research and to my wife Bethany forher patience.

Table of Contents

1 Introduction

1

2 Continuation marks

4

2.0.1

Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

53 λ-calculus

8

4 λv and λcm

11

4.1

λv

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

11

4.2

λcm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

11

5 CPS transformation

14

5.1

Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

14

5.2

Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

16

6 C

18
6.0.1

Intuition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

18

6.0.2

Concept . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

19

6.0.3

Initiation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

21

6.0.4

Some Final Subtleties . . . . . . . . . . . . . . . . . . . . . . . . . . .

22

6.0.5

Definition of C . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

22

6.0.6

Definition of C in CPS . . . . . . . . . . . . . . . . . . . . . . . . . .

24

6.0.7

Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

25iv

7 Testing

29

7.1

Redex . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

29

7.1.1

Toy Language . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

29

Flavors of λ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

33

7.2.1

λv . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

34

7.2.2

λcm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

35

Transformation definition . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

36

7.3.1

Direct Style . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

36

7.3.2

Continuation-passing Style . . . . . . . . . . . . . . . . . . . . . . . .

37

Transformation testing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

39

7.2

7.3

7.4

8 Proof40

9 Conclusion

45

References

46

A Proof of Lemma 1

48

A.1 Application Form . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

48

A.2 wcm Form . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

53

A.3 ccm Form . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

57

A.4 Value Form . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

58

A.5 Variable Form . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

60

B Reductions

63

B.1 Application Form . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

63

B.2 wcm form . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

64

B.3 ccm form . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

66

B.4 Value Form . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

66

B.5 Variable Form . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

67v

Chapter 1
Introduction

Thesis: A CPS-like global transformation can compile the λ-calculus with continuation
marks into the plain λ-calculus in a semantics-preserving way.
Numerous programming language instruments rely on stack inspection to function.
Statistical profilers sample the stack regularly to record active functions, algebraic steppers
observe the stack to represent the evaluation context of an expression, and debuggers naturally
require consistent access to the stack. Each of these relies on implementation-specificinformation and must be maintained as the instrumented language undergoes optimizationsand ventures across platforms. This makes these tools brittle and increases the porting
cost of the language ecosystem. Each of these examples would benefit from a generalized
stack-inspection mechanism available within the instrumented language itself. If written insuch an enhanced language, each instrument would be more robust, more easily modified,
and would port for free.
Continuation marks [4] are a programming language feature which generalizes stack
inpection. Not only do they dramatically simplify correct instrumentation [6], they havebeen used to allow inspection-based dynamic security checks in the presence of tail-call
optimization [5] and to express aspect-oriented programming in higher-order languagues [16].
In spite of their usefulness, continuation marks have remained absent from programming languages at large. One reason for this is that retrofitting virtual machines toaccommodate the level of stack inspection continuation marks must provide is expensive,
especially when the virtual machines use the host stack for efficiency.

1For example, the ubiquitous JavaScript is an ideal candidate for the addition ofcontinuation marks. However, as the lingua franca of the web, it has numerous mature
implementations which have been heavily optimized; to add continuation marks to JavaScript
amounts to modifying each implementation upstream, to say nothing of amending the
JavaScript standard. (Clements et al. successfully added continuation marks in Mozilla’s
Rhino compiler [7], but it remains a proof-of-concept.)
To avoid this roadblock, we instead take a macro-style approach; that is, we enhance
the core language with facilities to manipulate continuation marks and desugar the enhanced
language back to the core. To make our desugaring transformation apply to many languages,
we define it over the λ-calculus, the common core of most higher-order languages. With
such a transformation, language semanticists do not need to reconcile the feature with otherfeatures in the language (provided they have already done so with λ) and their compiler
writers do not need to worry about complicating their implementations (for the same reason).
The λ-calculus is a Turing-complete formal logic based on variable binding and substitution. Where the Turing machine model of computation is machine-centric, the λ-calculus
model is language-centric. Thus, it conveniently serves as an intermediate representation for
a compiler or a base from which to define higher-level languages. The standard reference tothe λ-calculus is Barendregt [2].
The continuation-passing style (CPS) transformation is actually a family of languagetransformations designed to make certain analyses simpler. Every member of this family
shares a common trait: their performance augments each function with an additional formal
parameter, the continuation, a functional representation of currently pending computation.
Functions in CPS never explicitly return; instead, they call the continuation argument with
their result. Because no function ever returns, function calls are the final act of the caller.
Thus, all calls are tail calls. The CPS transformation then simplifies programs by representing
all control and data transfer uniformly and explicitly. In general, the “spirit” of the CPS
transformation is to represent all transfers of control uniformly [15].

2We take the core of computation, the λ-calculus, and add facilities to manipulatecontinuation marks. These two together comprise a language which we term λcm . By
expressing λcm in terms of the plain λ-calculus, we uncover the meaning of continuation
marks in a pure computational language absent other language features and implementation
details. To do this, we construct C, a transformation from λcm programs to λ-calculus
programs in the spirit of CPS. We use Redex [8] to test candidate transformations forcorrectness. This allows us to increase our confidence in a functioning transformation but
cannot demonstrate correctness. We address this shortcoming by providing and proving ameaning preservation theorem.

3

Chapter 2
Continuation marks

There are certain tools that are indispensable to some programmers that concern
the behavior of their programs: debuggers, profilers, steppers, etc. Without these tools,
these programmers cannot justify the adoption of a language, however compelling it mightotherwise be. Traditionally, these tools are developed at the same level the language is,privy to incidental implementation detail, precisely because that detail enables these tools tofunction. This is problematic for at least two reasons. First, it couples the implementationof the tool with the implementation of the language, which increases the cost to port toother platforms. If users become dependent upon these tools, it can stall the advancementof the language and the adoption of new language features. Second and more critical, it
makes these tools unsound. For instance, debuggers typically examine programs which havebeen compiled without optimizations. In general, this means that the debugged program has
different behavior than the deployed program. This is obviously undesirable.
It is desirable to implement such tools at the same level as the language, removing
dependency upon the implementation and instead relying on definitional and behavioral
invariants. Continuation marks are a language-level feature that provide the informationnecessary for these tools to function. Furthermore, languages which require stack inspection
to enforce security policies (Java, C#) or support aspect oriented programming (aspectj ) canbe defined in terms of a simpler language with continuation marks [5, 16].
Continuation marks originated in PLT Scheme (now Racket [10]) as a stack inspection
mechanism. In fact, the Java and C# languages rely on a similar stack inspection to enforce4security policies of which continuation marks can be seen as a generalization. Surprisingly,
continuation marks can be encoded in any language with exception facilities [13].
The feature of continuation marks itself is accessible via two surface level syntactic
forms: with-continuation-mark and current-continuation-marks.
In Scheme-like syntax, a with-continuation-mark expression appears as (withcontinuation-mark key-expr value-expr body-expr ). The evaluation of this expression
proceeds by first evaluating key-expr to key and value-expr to value. Thereafter, body-expr isevaluated during which value is associated with key.
In the same Scheme-like syntax, a current-continuation-marks expression appearsas (current-continuation-marks key-list). This expression evaluates to a list of all thepresent key-value associations referenced in key-list. The with-continuation-mark form
admits a notion of ordering–inner associations are more recent than outer ones–and this inreflected in the list yielded by the current-continuation-marks.
Importantly, the result of current-continuation-marks provides no evidence of any
portion of the dynamic context lacking continuation marks with the specified keys. This
preserves the ability to perform optimizations without exposing details which would render the
optimizations unsound. This also requires special consideration of a language that supports
tail call optimization (which is not an optimization in the above sense since its behavior isdefined in the semantics of the language).

2.0.1

ExampleThe canonical example to illustrate the behavior of continuation marks in the presence andabsence of tail call optimization is the factorial function.
Figure 2.1 illustrates the properly recursive variant of the factorial function. In thisvariation, a cascade of multiplication operations builds as the recursive calls are made. Eachmultiplication is pending computation of which the machine must keep track.

5

(define (fac n)(if (= n 0)
1(∗ n (fac (− n 1)))))
Figure 2.1: The definitionally recursive factorial function(define (fac-tr n acc)
(if (= n 0)
acc
(fac-tr (− n 1) (∗ n acc))))Figure 2.2: A tail-recursive variant of the factorial function
Figure 2.2 illustrates the tail recursive variant of the factorial function. In contrast to
the function in figure 2.1, this variation performs the multiplication before the recursive call.
Because the function has no pending computations after the evaluation of the recursive call,the execution context need not grow. Such a call is said to be in tail position.
Figures 2.3 and 2.4 represent these two variants of the factorial function augmented
with continuation marks. Using these definitions, the result of (fac 3) would be(((fac 1)) ((fac 2)) ((fac 3)))6
whereas the result of (fac-tr 3 1) would be(((fac 1)))
6

(define (fac n)(if (= n 0)
(begin(display (current-continuation-marks ’(fac)))1)(with-continuation-mark ’fac n (∗ n (fac (− n 1)))))
Figure 2.3: The definitionally recursive factorial function augmented with continuation
marks

6

(define (fac-tr n acc)
(if (= n 0)
(begin(display (current-continuation-marks ’(fac)))acc)(with-continuation-mark ’fac n (fac-tr (− n 1) (∗ n acc))))Figure 2.4: The tail-recursive factorial function augmented with continuation marks
This difference is due to the growing continuation in the properly recursive fac. Eachcall to fac has a pending computation–namely, the multiplication–after the recursive call andso each necessitates the creation of additional evaluation context. The effect of this additional
context is that each annotation is applied to new, “blank” context, so all the previous
annotations are preserved. In the tail-recursive variant, there is no pending computation andtherefore no additional evaluation context. In this instance, the previous mark is overwrittenwith the new.

7

Chapter 3
λ-calculus

The λ-calculus [2] is a Turing-complete system of logic extensively used as a formal
system for expressing computation. Terms in the λ-calculus are defined inductively; theytake the form of variables x drawn from an infinite set, abstractions (λ (x) M ) where M isitself a λ-calculus term, and applications (M N ) where M and N are λ-calculus terms.
Variables in the λ-calculus are either free or bound. A variable x is free if it does notreside in the scope of a binding instance of x. Otherwise, x is bound. Terms with no freevariables can be called closed terms, combinators, or programs. The fact that variables are
drawn from an infinite set means that, given an arbitrary λ-calculus term, we can always
obtain a fresh variable, a variable not present in the term at hand. This is critical as we will
see shortly.
In an abstraction of the form (λ (x) M ), x is a binding instance which binds all freeoccurrences of x in the body M . To a first approximation, abstractions are functions. For
instance, the identity function can be expressed as (λ (x) x) where x is any variable. Thus,
there are an infinite number of ways to express the identity function: (λ (x) x), (λ (y) y),(λ (z) z), etc. A consequence of this is that terms which are not syntactically equivalent may
be semantically equivalent. This fact naturally gives rise to the notion of α-equivalence which
captures the idea that consistent renaming of bound variables, and their binding instances,does not change the meaning of a term.
There is some subtlety in valid renaming as there is the possibility of variable capture
which occurs when the new name of a binding instance is identical to that of some variable8already present in the body. For instance, in the term (λ (x) y), if each x is renamed to y, we
obtain the term (λ (y) y), a fundamentally different term. For this reason, we need to takespecial care when we rename variables, which we will need to do regularly.
One of the ways abstractions approximate functions is that we can apply them toarguments. This is signified simply by juxtaposition of function (or operator) and argument(or operand). In the correct context, an application of the form (M N ) can be reduced inwhich the operator M is applied to the operand N . For M of the form (λ (x) M 0 ) for someM 0 , this entails the substitution of every free occurrence of x in M 0 with N . The notation
we adopt for this is M 0 [x ← N ]. For instance, the application ((λ (x) x) y) signifies x[x ← y]and so reduces to y. Here, we must protect against another strain of variable capture. As
an example, consider the reduction of ((λ (x) (λ (y) x)) y). If we reduce naively, we obtain(λ (y) y) which does not reflect the intended meaning of the reduction–the argument y has
been captured by the abstraction, an act which destroys its meaning within the environment.
In order to avoid this, we must rename capturing abstractions in M to be outside the setof free variables of N . Within the greater term ((λ (x) (λ (y) x)) y), we rename y to z in
(λ (x) (λ (y) x)) obtaining (λ (x) (λ (z) x)). The subsequent reduction of ((λ (x) (λ (z) x)) y)to (λ (z) y) correctly reflects the intended meaning of the original term.
In the λ-calculus, evaluation occurs during reduction, and reduction is merely application. There is, however, yet more subtlety of which we must be aware: namely, in which
contexts applications are performed and terms evaluated. In the call-by-value λ-calculus,
denoted λv , evaluation of operands occurs before application. In contrast, in the call-by-nameλ-calculus, denoted λn , application is performed as soon as the operator is resolved.
For instance, in ((λ (x) x) ((λ (y) y) (λ (z) z))),((λ (x) x) ((λ (y) y) (λ (z) z)))→λv ((λ (x) x) (λ (z) z))→λv (λ (z) z)

9whereas((λ (x) x) ((λ (y) y) (λ (z) z)))→λn ((λ (y) y) (λ (z) z))→λn (λ (z) z)

Although both terms reduce to the same term in this example, this distinction is not merely
pedantic: terms may reduce definitively in one reduction regime and fail to reduce completely
in the other! Consider ((λ (x) (λ (y) y)) ((λ (x) (x x)) (λ (x) (x x)))) where((λ (x) (λ (y) y)) ((λ (x) (x x)) (λ (x) (x x)))) →λn (λ (y) y)but((λ (x) (λ (y) y)) ((λ (x) (x x)) (λ (x) (x x))))→λv ((λ (x) (λ (y) y)) ((λ (x) (x x)) (λ (x) (x x))))→λv · · ·Historically at least, the call-by-name and call-by-value reduction regimes underlie thedistinction between so-called lazy and eager languages.
One final observation we should make about the λ-calculus is which terms denotevalues. A value should be, in a sense, irreducible and that criterion disqualifies applications
from being considered as values. A value should should not merely be a placeholder for
arbitrary values, and that criterion disqualifies lone variables from being considered as values.1
Thus, we shall consider abstractions to be the sole form values can take in the λ-calculus,
habituating ourselves to the idea that functions are data.
1
To be precise, a value is a closure: an irreducible λ-calculus term paired with an environment which
provides values for constituent free variables.

10Chapter 4
λv and λcm

4.1

λv

The λv language is merely the call-by-value λ-calculus [14].
Figure 4.1 presents the language terms and evaluation contexts of λv . The definitionof e specifies the form of terms in λv similar to our previous discussion of the λ-calculus. The
definition of E specifies evaluation contexts which, like terms, are defined inductively. An
evaluation context is either empty (denoted by •), an application wherein the operator isbeing evaluated, or an application wherein the operand is being evaluated.
Figure 4.2 presents the sole semantic definition of λv , the meaning of application.

4.2

λcm

We now consider an extension of λv with facilities to manipulate continuation marks, introduced by Pettyjohn et al. [13], which we term λcm . As an extension of λv , it inherits its
definitions of language terms, evaluation contexts, and semantics.

E =(E e)(v E)•

e =(e e)xvv =(λ (x) e)
Figure 4.1: λv forms

11E[(λx.e) v] → E[e[x ← v]]

Figure 4.2: λv evaluation rule

E =(wcm v F )
F
F =•
(E e)
(v E)
(wcm E e)e =(e e)xv
(wcm e e)(ccm)
v =(λ (x) e)

Figure 4.3: λcm forms
Figure 4.3 presents the syntactic forms of λcm . Definitions of E and F signify evaluation
contexts. The separation of E from F prevents (wcm v F ) contexts from directly nesting
within the entire evaluation context to enforce proper tail-call behavior. The definition of e
is identical to that of λv with the addition of contionuation mark forms (wcm e e) and (ccm).
(λcm expresses unkeyed marks which obviates the need to specify a key to which a value will
be associated. Hence, the wcm and ccm forms need one parameter fewer than their Schemecounterparts.)
Figure 4.4 presents the semantics of λcm in the form of a list of reduction rules. Rule
1 defines the meaning of application as inherited from λv . Rule 2 defines the tail behavior of
the wcm form. Rule 3 expresses that the wcm form takes on the value of its body. Finally,rule 4 defines the value of the ccm form in terms of the χ metafunction.
The definition of the χ-metafunction is given in figure 4.5. Conceptually, the χmetafunction traverses the context from the outside in, accumulating values as it encounters(wcm v E) contexts. Since the χ metafunction is defined over evaluation contexts of λcm , itsdomain corresponds to the definitions of E and F in figure 4.3.

12

E[(λx.e) v] → E[e[x ← v]]
E[(wcm v (wcm v 0 e))] → E[(wcm v 0 e)]
E[(wcm v v 0 )] → E[v 0 ]E[(ccm)] → E[χ(E)]

(1)
(2)
(3)
(4)

Figure 4.4: λcm semantics

χ(•) = nilχ(E[(• e)]) = χ(E)
χ(E[(v •)]) = χ(E)
χ(E[(wcm • e)]) = χ(E)
χ(E[(wcm v •)]) = v : χ(E)Figure 4.5: Definition of χ metafunction
In λcm , evaluation of an application form proceeds asE[(e0 e1 )] →λcm E[(• e1 )][e0 ]→∗λcm E[(• e1 )][v0 ]→λcm E[(v0 e1 )](1)→λcm E[(v0 •)][e1 ]→∗λcm E[(v0 •)][v1 ]→λcm E[(v0 v1 )](2)=E[((λ (x) e00 ) v1 )]for some x and e00→λcm E[e00 [x ← v1 ]]=E[e2 ]

for some e2

Steps 1 and 2 denote the insertion of a value into the hole in the context.

13

Chapter 5
CPS transformation

5.1

Introduction

The CPS transform is actually a family of language transformations derived from Plotkin[14] designed to simplify programs by representing all data and control flow uniformly andexplicitly. This, in turn, simplifies compiler construction and analyses such as optimizationand verification [1, 15]. The standard variation of CPS adds a formal parameter to every
function definition and an argument to every call site.
As an example, consider once again the two variants of the factorial function, sanscontinuation marks, given earlier. In CPS, the properly-recursive variant can be expressed as(define (fac n k )(if (= n 0)
(k 1)
(fac (− n 1) (λ (acc) (k (∗ n acc))))))and the tail-recursive variant as(define (fac-tr n acc k )(if (= n 0)
(k acc)(fac-tr (− n 1) (∗ n acc) k )))(For clarity, we have treated “primitive” functions–equality comparison, subtraction, andmultiplication–in a direct manner. In contrast, a comprehensive CPS transformation would
affect every function.)
Notice that, in the first variation, each recursive call receives a newly-constructed k
encapsulating additional work to be performed at the completion of the recursive computation.
14

In the second, k is passed unmodified, so while computation occurs within each context, no
additional computation pends. From this example, we see that the CPS representation is
ideal for understanding tail-call behavior as it is explicit that the continuation is preservedby the tail call.
The purpose of CPS does not lie solely in pedagogy, however. The reification of andconsequent ability to directly manipulate the continuation is powerful, analogous in power
to the ability to capture a continuation which some languages provide. In Scheme, this isaccomplished with call/cc, short for “call with current continuation”. This call takes one
argument which itself is a function of one argument. call/cc calls its argument, passing in afunctional representation of the current continuation–the continuation present when call/cc
was invoked. This continuation function takes one argument which is treated as the result ofcall/cc and runs this continuation to completion.
As a simple example,(+ 1 (call/cc(λ (k )(k 1))))
returns 2. In effect, invoking k with 1 is the same as replacing the entire call/cc
invocation with 1.
Much of the power of call/cc lies in the manifestation of the continuation as a function,
giving it first-class status. It can be passed as an argument in function calls, invoked, and,amazingly, reinvoked at leisure. It is this reinvokeability that makes call/cc the fundamental
unit of control from which all other control structures can be built, including generators,
coroutines, and threads.
In direct style, the definition of call/cc is conceptually(define call/cc(λ (f )(f (get-function-representing-continuation))))15

where get-function-representing-continuation is an opaque function which leverages sweeping knowledge of the language implementation. The CPS definition is notably
simpler:(define call/cc(λ (f k )(f (λ (x w ) (k x )) k )))Within the definition of call/cc, we define an anonymous function which, when givena value x and continuation w, applies the captured continuation k to x.
Variations of the standard CPS transformation make the expression of certain control
structures more straightforward. For instance, the “double-barrelled” CPS transformation
is a variation wherein each function signature receives not one but two additional formal
parameters, each a continuation. One application of this particular variation is error handlingwith one continuation argument representing the remainder of a successful computation andthe other representing the failure contingency. It is especially useful in modelling exceptions
and other non-local transfers of control in situations where the computation might fail. In
general, the nature of the CPS transformation allows it to untangle complicated, intricate
control structures.
Similar transformations exist which express other programming language features suchas security annotations [17] and control structures such as procedures, exceptions, labelledjumps, coroutines, and backtracking. On top of other offerings, this places it in a category oftools to describe and analyze programming language features. (This category is also occupied
by Moggi’s computational λ-calculus–monads [12].)

5.2

ExampleWe will now focus our attention on a CPS transform defined over λv .
A CPS transformation is a global syntactic transformation of language terms. Recall
that terms in the λ-calculus take the form of lone variables x, λ-abstractions (λ (x) M ), and16

applications (M N ) where M and N are themselves λ-calculus terms. A comprehensive CPS
transform definition then need only specify transformations for these three categories. As an
example, consider Fischer’s CPS transform [9]:F[x] = (λ (k) (k x))
F[(λ (x) M )] = (λ (k) (k (λ (x) F[M ])))
F[(M N )] = (λ (k) (F[M ] (λ (m) (F[N ] (λ (n) ((m n) k))))))

Fischer’s CPS transform abstracts each term in the λ-calculus: lone variables wait on acontinuation, abstractions receive a degree of indirection, and even applications, the sole
reduction facility of the λ-calculus, become abstractions. In essence, terms become suspended
in wait of a continuation argument. By priming a term so-transformed with a continuation
function–even as simple as the identity function–we instigate a cascade of computation.
In a sense, the CPS transform contaminates abstractions, the values of the λ-calculus.
For example, consider the transformation of λx.x

F[λx.x] = λk.k (λx.F[x])= λk.(k λx.λk.(k x))

If we apply this term to the identity function, it reduces as

λk.(kλx.λk.(k x)) λy.y
→λv λy.y λx.λk.(k x)→λv λx.λk.(k x)

The result of this reduction contains residue of the CPS transform. This must be accounted
for when attempting to formally relate direct and continuation-passing style terms.

17Chapter 6C

A CPS-like global transformation can compile the λ-calculus with continuation marks
into the plain λ-calculus in a semantics-preserving way.
In order to demonstrate this, we must first clarify (and later, formalize) the semanticspreservation property. We will define a transformation from λcm to λv and term it C, as incompile, since we are, in essence, compiling away continuation marks. In order to preserve
the meaning of λcm , C must commute with evaluation. More precisely, C satisfies
p

→∗λcm

↓C
C[p]

v
↓C

→∗λv

C[v]

for any program p ∈ λcm .
The burden of demonstration is then reduced to the existence of C. We do this byconstruction.

6.0.1

Intuition

The essence of λcm is that programs can apply information to and observe information
about the context in which they are evaluated. Programs in λv have no such facility. We
can simulate this facility by explicitly passing contextual information to each term as it isevaluated. We can define C to transform wcm directives to manipulate this information andccm directives to access it. Intuitively, we can transform λcm programs to mark-passing style.

18

However, marks alone do not account for the tail-call behavior specified by rule 2 of
figure 4.4. Since tail-call behavior is observable (if indirectly) by λcm programs, we must also
provide to each term information about the position in which it is evaluated. Specifically,each transformed wcm directive must be notified whether it is evaluated in tail position ofan enclosing wcm directive as it must behave specially if so. Thus, in addition to passing thecurrent continuation marks, the transform should pass a flag to each term indicating whether
it is evaluated in tail position of a wcm directive.
These two pieces of information suffice to correctly simulate continuation marks.

6.0.2

Concept

The definition of C entails transformation over each syntactic form of λcm .
With this in mind, consider a conceptual transformation of application, C[(rator-expr
rand-expr )], as(λ (flag)(λ (marks)(let ((rator-value ((C[rator-expr ] false) marks))(rand-value ((C[rand-expr ] false) marks))(((rator-value rand-value) flag) marks))))ignoring for the moment that let is in neither λv or λcm . This definition captures that
1. before evaluation, we expect flag to indicate tail position information and marks toprovide a list of the current continuation marks,
2. we would like to evaluate C[rator-expr ] and C[rand-expr ] in the same manner, providing
to each its contextual information–specifically that neither is evaluated in tail positionof a wcm directive and the continuation marks for each are unchanged from the parent
context, and3. following evaluation of operator and operand and application, evaluation of the resultant
term is performed with the original contextual information.

19

Now consider a conceptual transformation of a wcm directive, C[(wcm mark-expr
body-expr )], as(λ (flag)(λ (marks)((C[body-expr ] true) (let ((mark-value ((C[mark-expr ] false) marks))(rest-marks (if flag (snd marks) marks)))(cons mark-value rest-marks)))))
with similar caveats as the previous case. This definition captures that
1. as in application, we expect flag to indicate tail position information and marks toprovide a list of the current continuation marks,
2. we evaluate mark-expr with correct contextual information,
3. we discard the first continuation mark of the parent context if evaluation is occurringin tail position of a wcm directive, and
4. we evaluate C[body-expr ] with the correct tail-position flag and current continuation
marks.
Finally, consider the conceptual transformation of a ccm directive, C[(ccm)], as(λ (flag)(λ (marks)
marks))
wherein we reap the fruits of simplicity from our laborious passing: this definition is
gratifyingly direct.
The conceptual transformation of variables x and values (λ (x ) e) is straightforward.
We now address the absence of let, if, cons, etc. from λv .
We can express the let construct in λv with application. An expression such as(let ((x 1 e 1 )...
(x n e n))e)20

Definition 1. true = (λ (x) (λ (y) x))
Definition 2. false = (λ (x) (λ (y) y))
Definition 3. cons = (λ (a) (λ (b) (λ (z) ((z a) b))))Definition 4. fst = (λ (p) (p true))
Definition 5. snd = (λ (p) (p false))
Definition 6. nil = false
Figure 6.1: Church encodings for booleans and lists.
can be interpreted as(. . . ((λ (x 1 ) . . . (λ (x n)e). . . ) e 1 ) . . . ) e n)which is the curried form of((λ (x 1 . . . x n)e) e 1 . . . e n)
We unfold this characterization of let to guide the construction of C before simplifying.
To achieve if and conditionals as well as list primitives cons, snd , and nil , we use the
Church encodings of fig. 6.0.2.

6.0.3

Initiation

Abstracting terms has the effect of suspending evaluation. When an entire program istransformed, all evaluation is suspended, and awaits arguments representing contextual
information. At the top level, the context is empty, so we pass the contextual information for
the empty context: false, indicating evaluation is not occurring in wcm tail position andnil, an empty list of marks.
We can accommodate this by defining a top-level transform Cˆ in terms of C by

ˆ = ((C[p] false) nil)
C[p]

21

(6.1)

and stating our commutativity property asˆˆC[evalcm (p)] = evalv (C[p])(6.2)((C[evalcm (p)] false) nil) = evalv (((C[p] false) nil))(6.3)

which is equivalent to

6.0.4

Some Final Subtleties

Our choice to keep the core language small by omitting lists as primitive values has theconsequence of complicating our transform somewhat. Because lists are defined in termsof λ-calculus values which are themselves touched by the transform and because of thecommutativity property that C must satisfy, we cannot deal with a list of continuation marks
directly–we must instead deal with a transformed list of transformed continuation marks,
and manipulation of this list within transformed terms must occur at the transformed level.
Additionally, after evaluation, values are “truncated” with their leading abstractions
applied away. For instance, the transformation of the value (λ (x ) x ) to (λ (flag) (λ (marks)(λ (x ) (λ (flag) (λ (marks) x ))))) will yield, following evaluation, (λ (x ) (λ (flag) (λ (marks)x ))). For convenience, we define

C 0 [(λ (x) e)] = (λ (x) C[e])(6.4)ˆ = ((C[p] false) C 0 [nil])
C[p]

(6.5)

and we adjust Cˆ so that

6.0.5

Definition of C

Finally, we present the definition of C over the five syntactic forms of λcm .
Definition 7. C[(rator-expr rand-expr )]22

The formal transformation of application follows the let version exactly except the definitionsof rator-value and rand-value are folded directly in.
(λ (flags)(λ (marks)(((((C[rator-expr ] false) marks)((C[rand-expr ] false) marks))
flags)
marks)))
Definition 8. C[(wcm mark-expr body-expr )]The formal transformation of a wcm directive is also extremely similar to the let version.
The definition of C[cons] is unfolded and simplified.
(λ (flag)(λ (marks)((C[body-expr ] true)(((λ (mark-value) (λ (rest-marks) Cˆcps [((cons mark-value) rest-marks)]))((C[mark-expr ] false) marks))
ˆ((flag C[(sndmarks)]) marks)))))
Definition 9. C[(ccm)]
The let version of the transformation of a ccm directive remains unchanged.
(λ (flag)(λ (marks)
marks))
Definition 10. C[v ]=C[(λ (x ) e)]
Like other terms, values are modified to receive contextual information. However, being
unaffected by context, values discard this information.
(λ (flag)(λ (marks)(λ (x ) C[e])))Definition 11. C[x ]23Variables have the property that, when substitution occurs, they reconstitute transformed
values. That is, in the midst of application in C, terms of the form (C 0 [(λ (x ) x )] C 0 [(λ (y)y)]) appear, reducing to C[x][x ← C 0 [(λ (y) y)]] = C[x[x ← (λ (y) y)] = C[(λ (y) y)].
(λ (flag)(λ (marks)
x ))

6.0.6

Definition of C in CPS

We present a continuation mark transformation integrated in CPS.
Definition 12. Ccps [(rator-expr rand-expr )](λ (kont)(λ (flag)(λ (marks)(((Ccps [rator-expr ](λ (rator-value)(((Ccps [rand-expr ](λ (rand-value)((((rator-value rand-value) kont) flag) marks)))
false) marks)))
false) marks))))Definition 13. C[(wcm mark-expr body-expr )](λ (kont)(λ (flag)(λ (marks)(((Ccps [mark-expr ](λ (mark-value)((λ (rest-marks)(((Ccps [body-expr ] kont) true) Cˆcps [((cons mark-value) rest-marks)]))((flag Cˆcps [(snd marks)]) marks))))false) marks))))Definition 14. Ccps [(ccm)](λ (kont)(λ (flag)24

(λ (marks)(kont marks))))Definition 15. Ccps [v ]=Ccps [(λ (x ) e)](λ (kont)(λ (flag)(λ (marks)(kont (λ (x ) Ccps [e])))))
Definition 16. Ccps [x ](λ (kont)(λ (flag)(λ (marks)(kont x ))))
ˆWe include corresponding definitions for C 0 and C.
0
Definition 17. Ccps[(λ (x ) e)](λ (x ) Ccps [e])Definition 18. Cˆcps [p]0[nil ])(((Ccps [p] (λ (x ) x )) false) Ccps

6.0.7

ExampleTo better illustrate what the transformation does, we step through the reduction of a program
which exhibits its more interesting aspects. One λcm program suited to this purpose is (wcm
0 ((λ (x ) (wcm x (ccm))) 1)). It reduces according to λcm semantics as(wcm 0 ((λ (x ) (wcm x (ccm))) 1))(wcm 0 (wcm 1 (ccm)))(wcm 1 (ccm))(wcm 1 (λ (z ) ((z 1) (λ (x ) (λ (y) y)))))(λ (z ) ((z 1) (λ (x ) (λ (y) y))))25

Now consider the reduction of the same program transformed. We apply the transformation just-in-time as we reduce to prevent term size explosion and promote clarity andomit uninteresting reductions.
ˆC[(wcm0 ((λ (x ) (wcm x (ccm))) 1))]
By definition this is((C[(wcm 0 ((λ (x ) (wcm x (ccm))) 1))] false) C 0 [nil])which explodes upon expansion to(((λ (flag)(λ (marks)((C[((λ (x ) (wcm x (ccm))) 1)] true)(((λ (mark-value) (λ (rest-marks) C 0 [((cons mark-value) rest-marks)]))ˆ((C[0] false) marks)) ((flag C[(sndmarks)]) marks)))))
0false) C [nil])
After the application of contextual information, we reach((C[((λ (x ) (wcm x (ccm))) 1)] true)(((λ (mark-value) (λ (rest-marks) C 0 [((cons mark-value) rest-marks)]))ˆ((C[0] false) C 0 [nil])) ((false C[(sndnil)]) C 0 [nil])))the transformation of the wcm body. Terms within are arranged so that correct evaluation
occurs within the native call-by-value regime. This evaluates mark-expr and and prepends
its value to the list of continuation marks before proceeding with evaluation of body-expr .
This reduction soon yields the following term:((C[((λ (x ) (wcm x (ccm))) 1)] true) C 0 [((cons 0) nil)])
It is evident that this term will behave exactly as a top-level term except as this contextual
information influences it, and this is exactly the property we have strived for. Expansion ofthis term yields(((λ (flag)(λ (marks)(((((C[(λ (x ) (wcm x (ccm)))] false) marks)((C[1] false) marks))
26

flag)
marks))) true) C 0 [((cons 0) nil)])the expansion of an application. In this example, both the operator and operand are values,
so are essentially unaffected by the application of contextual information; this application
has the effect of preparing the terms for application:((((λ (x ) C[(wcm x (ccm))])1) true) C 0 [((cons 0) nil)])
reduces to((C[(wcm 1 (ccm))]true) C 0 [((cons 0) nil)])This expands and reduces as the wcm term seen previously:(((λ (flag)(λ (marks)((C[(ccm)] true)(((λ (mark-value) (λ (rest-marks) C 0 [((cons mark-value) rest-marks)]))((C[1] false) marks))
ˆ((flag C[(sndmarks)]) marks)))))
0true) C [((cons 0) nil)])
Of interest in this process is the effective collapse of the previous mark context by
virtue of the value of flag. When we reach((λ (marks) marks)((λ (rest-marks) C 0 [((cons 1) rest-marks)])
ˆ((true C[(snd((cons 0) nil))]) C 0 [((cons 0) nil)])))
the list is beheaded to simulate mark overwriting:((λ (marks) marks)((λ (rest-marks) C 0 [((cons 1) rest-marks)])ˆC[(snd((cons 0) nil))]))
Once given the contextual information, the evaluation of ccm is simple:((λ (marks) marks)
C 0 [((cons 1) nil)])27

reduces to
C 0 [((cons 1) nil)]
and we are left with just what we hoped for.

28

Chapter 7
Testing

We do not attempt to construct a correct transformation ex nihilo. A pragmatic
approach to the discovery of a correct transformation involves consistent feedback and testing
to validate candidate transforms. Testing is no substitute for proof, but, as Klein et al. [11]show, proof is no substitute for testing. Lightweight mechanization is a fruitful middle groundbetween pencil-and-paper analysis and fully- mechanized formal proof. We use Redex toprovide feedback, thoroughly exercise candidates, and perform exploratory analysis.

7.1

Redex

Redex [8] is a domain-specific language for exploring language semantics. It lives very close
to the semantics notation we have used so far in this discussion.

7.1.1

Toy Language

To illustrate how easily langagues can be defined in Redex, we will examine a Redex program
which defines a toy language. In contrast to a Redex tutorial, we will not concern ourselveswith the syntax and structure of roads not taken and will instead briefly explain eachcomponent of the program.
(define-language toy(x variable-not-otherwise-mentioned)(v number undefined)(e (+ e e) (with (x e) e) x v )(E • (+ E e) (+ v E ) (with (x E ) e)))29

This expression defines the abstract syntactic structure of a language named toy.
There are four categories of structures: x , v , e, and E . The category x is defined to containany token not otherwise mentioned in the definition. The category v is defined to contain
numbers and the token undefined. The category e is defined to contain the expression forms of
the language, of which there are four: addition expressions, with expressions, lone variables,
and lone values. The last category, E , does not define abstract syntax but instead reduction
contexts. The first reduction context is a • (a special token in Redex) which will be filledin with the result of the expression that previously resided in its place. The next two are
addition contexts, the first representing the evaluation of the first argument and the second
representing the evaluation of the second; the composition of these contexts imposes an orderon the evaluation of the arguments. The final context, a with context, specifies a variable, avalue, and an expression within which that variable is bound to that value.
(define toy-rr(reduction-relation toy(→ (in-hole E (+ number 1 number 2 ))(in-hole E (+ (term number 1 ) (term number 2 )))"+")(→ (in-hole E (with (x 1 v 1 ) e 1 ))(in-hole E (substitute x 1 v 1 e 1 ))"with")(→ (in-hole E x 1 )(in-hole E undefined)"free variable")(→ (in-hole E (+ undefined e 1 ))(in-hole E undefined)"undefined in first position")(→ (in-hole E (+ number 1 undefined))(in-hole E undefined)"undefined in second position")))This term defines a reduction relation on the toy language. The five defined reductions,signalled by →, match specified patterns and manipulate them according to the defined rules.
These define: the addition of two numbers; the substitution of a with expression; a lone30

variable; the addition of an undefined value on the left; and the addition of an undefinedvalue on the right.
(define-metafunction toy
substitute : x v e -> e[(substitute x 1 v 1 (+ e 1 e 2 ))(+ (substitute x 1 v 1 e 1 ) (substitute x 1 v 1 e 2 ))][(substitute x 1 v 1 (with (x 1 e 1 ) e 2 ))(with (x 1 (substitute x 1 v 1 e 1 )) e 2 )][(substitute x 1 v 1 (with (x 2 e 1 ) e 2 ))(with (x 2 (substitute x 1 v 1 e 1 )) (substitute x 1 v 1 e 2 ))][(substitute x 1 v 1 x 1 )v 1][(substitute x 1 v 1 x 2 )x 2][(substitute x 1 v 1 v 2 )v 2 ])The definition of the with reduction rule relies on the substitute metafunction. (Thelanguage used to define toy (Redex) is the metalanguage. As functions are in the language,
metafunctions are in the metalanguage.) The substitute metafunction recursively substitutes
a variable in an expression with a value. The substitution is only propagated as long as abinding with the same name is not encountered. At that point, the substitution is performedin the value expression of the binding, but not the body. This allows for expressions like(with (x 5)(with (x x )x ))to behave as we expect (returning 5).

Testing
Now that the syntactic forms and reduction rules of the language are defined, we can use therandomized testing built into Redex to investigate properties of the language. We start bydefining the helper function(define (reduces-to-one-value? e)31

(let ((results (apply-reduction-relation∗ toy-rr e)))(and (= (length results) 1)(value? (first results)))))
which has its own helper function(define value? (redex-match toy v ))The ∗ at the end of the function name apply-reduction-relation∗ signifies that all
possible reduction rules will be applied as many times as possible. If some of the reduction
rules don’t actually reduce terms, the relation may produce a reducible term indefinitely.
The function apply-reduction-relation∗ is in a sense strict in the reduction relation andwill likewise run indefinitely if this is the case.
After the language and some properties have been established, the randomized testing,initiated by(redex-check toy e (reduces-to-one-value? (term e)))is simple. We merely provide the name of the language we wish to work with, the nonterminalin the grammar we wish to use to generate language terms, and a predicate that checks
terms for properties. This function generates terms gradually increasing in size, applying thepredicate to each in turn, and terminates with a counterexample or after a set number ofterms have been checked (1000 by default).

Proof
Randomized testing can increase our confidence in various assertions but is no substitute for
proof. We express the property of reducing to one value with the following theorem:
Toy Language One-Value Theorem. For all terms e of the toy language, e reduces toexactly one value.1
1

We do not use the term value loosely here; the toy language definition specifies what constitute values,
and we appeal to this.

32

We proceed by induction on the structure of terms e of the toy language. First, weconsider the base cases.
Case v . A term e of the form v is exactly one value and cannot be reduced, so the statement
holds.
Case x . A term e of the form x , a variable, reduces to undefined, a value term, so thestatement holds.
Case (with (x e 1 ) e 2 ). By induction, we assume that e 1 reduces to exactly one value.
Then the “with”-rule can only be applied once, resulting in a single term e 2 in e which, by
our inductive hypothesis, reduces to only one value.
Case (+ e 1 e 2 ). By induction, we assume both e 1 and e 2 reduce to a single value. We
consider two subcases: If e 1 reduces to undefined, the “undefined in first position”-rule isapplied, and the whole term reduces to undefined. If e 1 reduces to a number, we consider
two further subcases: If e 2 reduces to a number, the “+”-rule is applied, and the entire
expression reduces to the sum of the two numbers obtained. If e 2 reduces to undefined, the“undefined in second position”-rule is applied, and the entire term reduces to undefined. Thus,in all subcases, the whole term reduces to exactly one value.
This property is fairly trivial and its proof is similarly trivial, but it is a shadow of
the approach we will ultimately take to verify certain transformation properties.

7.2

Flavors of λOur first task in developing a testing environment for transformations is to define interpretersfor λcm and λv .
We begin with λv , the simpler language.

33

7.2.1λv

To begin, we define language terms and evaluation contexts.
(define-language λv(e (e e) x v error)(x variable-not-otherwise-mentioned)(v (λ (x ) e))(E (E e) (v E ) •))The characterization of λv seen in figures 4.1 and 4.2 was influenced by the knowledge
that an interpreter would need to be built. Because Redex lives so close to this characterization,
the only change we make in translation is the addition of error.
(define λv-rr(reduction-relation λv(→ (in-hole E ((λ (x ) e) v ))(in-hole E (λv-subst x v e))"betav")(→ (in-hole E x )(in-hole E error)"error: unbound identifier")(→ (in-hole E (error e))(in-hole E error)"error in operator")(→ (in-hole E (v error))(in-hole E error)"error in operand")))The first rule in the reduction relation corresponds with the sole semantic rule foundin 4.2. The remaining handle cases introduced by error.
(define-metafunction λv
λv-subst : x v e -> e;; 1. substitute in application[(λv-subst x 1 v 1 (e 1 e 2 ))((λv-subst x 1 v 1 e 1 ) (λv-subst x 1 v 1 e 2 ))];; 2a. substitute in variable (same)[(λv-subst x 1 v 1 x 1 )v 1];; 2b. substitute in variable (different)[(λv-subst x 1 v 1 x 2 )
34

x 2]
;; 3a. substitute in abstraction (bound)[(λv-subst x 1 v 1 (λ (x 1 ) e 1 ))(λ (x 1 ) e 1 )];; 3b. substitute in abstraction (free)[(λv-subst x 1 v 1 (λ (x 2 ) e 1 ))(λ (x 2 ) (λv-subst x 1 v 1 e 1 ))];; 4. substitute in error[(λv-subst x 1 v 1 error)
error])The λv-subst metafunction presents the conceptual definition of substitution. Because
we generate fresh identifiers within the transform, we don’t need to worry about capture
avoidance.

7.2.2

λcm

Since λcm is a superset of λv , we need only extend the definition of the λv interpreter toaccommodate the additions λcm brings.
(define-extended-language λcm λv(e .... (wcm e e) (ccm))(E (wcm v F ) F )(F (E e) (v E ) (wcm E e) •))Redex allows us to easily define a proper extension of a language, inheriting anythingleft unspecified. As similar as the λv interpeter definition is to the λv definition in figure 4.1,
this λcm interpreter definition is to the λcm definition in figure 4.3.
(define λcm-rr(extend-reduction-relation λv-rr λcm(→ (in-hole E ((λ (x ) e) v ))(in-hole E (λcm-subst x v e))"betav")(→ (in-hole E (wcm v 1 (wcm v 2 e)))(in-hole E (wcm v 2 e))"wcm-collapse")(→ (in-hole E (wcm v 1 v 2 ))(in-hole E v 2 )"wcm")35

(→ (in-hole E (ccm))(in-hole E (chi E (λ (x ) (λ (y) y))))"chi")(→ (in-hole E (wcm error e))(in-hole E error)"error in wcm mark expression")(→ (in-hole E (wcm v error))(in-hole E error)"error in wcm body expression")))The first three rules in the reduction relation correspond with the three additionalsemantic rules found in 4.4. The remaining handle cases introduced by the the new language
forms’ interaction with error.
(define-metafunction/extension λv-subst λcm
λcm-subst : x v e -> e;; 1. substitute in wcm form[(λcm-subst x 1 v 1 (wcm e 1 e 2 ))(wcm (λcm-subst x 1 v 1 e 1 ) (λcm-subst x 1 v 1 e 2 ))];; 2. substitute in ccm form[(λcm-subst x 1 v 1 (ccm))(ccm)])The λcm-subst metafunction is extended to accommodate the additional forms in λcm .
(define-metafunction λcm
chi : E v -> v[(chi • v ms)
v ms][(chi (E e) v ms)(chi E v ms)](chi E v ms)][(chi (v E ) v ms)[(chi (wcm E e) v ms) (chi E v ms)][(chi (wcm v E ) v ms) (chi E (λ (p) ((p v ) v ms)))])
Finally, we define the χ metafunction. Its definition does not map directly to theformal definition, but matches the intuitive definition that underlies it.

7.3
7.3.1

Transformation definition
Direct Style(define (c e)36

(let ([flag (gensym ’f)][marks (gensym ’m)][mark-value (gensym ’a)][rest-marks (gensym ’r)])(match e[(list ’ccm)‘(λ (,flag)(λ (,marks),marks))][(list ’wcm mark-expr body-expr )‘(λ (flag)(λ (marks)((,(c body-expr ) (λ (x) (λ (y) x)))(((λ (,mark-value) (λ (,rest-marks) ,(c-hat ‘(λ (z) ,(c ‘((z ,mark-value) ,rest-marks))))))((,(c mark-expr ) (λ (x) (λ (y) y))) ,marks))((flag ,(c-hat ‘((λ (p) (p (λ (x) (λ (y) y)))) ,marks))) ,marks)))))][(list ’λ (list x0 ) e0 )‘(λ (,flag)(λ (,marks)(λ (,x0 ),(c e0 ))))][(list rator-expr rand-expr )‘(λ (,flag)(λ (,marks)(((((,(c rator-expr ) (λ (x) (λ (y) y))) ,marks)((,(c rand-expr ) (λ (x) (λ (y) y))) ,marks)),flag),marks)))][’error’error][x0‘(λ (flag) (λ (marks) ,x0 ))])))(define (c-hat e)(let ([f (gensym ’f)][m (gensym ’m)])‘((,(c e) (λ (x) (λ (y) y))) (λ (x) ,(c ’(λ (y) y))))))
7.3.2

Continuation-passing Style(define (c-cps e)(let ([kont (gensym ’k)][flag (gensym ’f)][marks (gensym ’m)]37

[rator-value (gensym ’t)][rand-value (gensym ’n)][rest-marks (gensym ’r)][a (gensym ’a)][b (gensym ’b)][f (gensym ’f)])(match e[(list ’ccm)‘(λ (,kont)(λ (,flag)(λ (,marks)(,kont ,marks))))][(list ’wcm mark-expr body-expr )‘(λ (,kont)(λ (,flag)(λ (,marks)(((,(c-cps mark-expr )(λ (,mark-value)((λ (,rest-marks)(((,(c-cps body-expr ),kont)(λ (x) (λ (y) x))),(c-hat ‘(λ (z) ((z ,mark-value) ,rest-marks)))))((flag ,(c-hat ‘((λ (p) (p (λ (x) (λ (y) y)))) ,marks))) ,marks))))(λ (x) (λ (y) y))),marks))))][(list ’λ (list x0 ) e0 )‘(λ (,kont)(λ (,flag)(λ (,marks)(kont (λ (,x0 ) ,(c-cps e0 ))))))][(list rator-expr rand-expr )‘(λ (,kont)(λ (,flag)(λ (,marks)(((,(c-cps rator-expr )(λ (,rator-value)(((,(c-cps rand-expr )(λ (,rand-value)((((,rator-value ,rand-value) ,kont) ,flag) ,marks)))(λ (x) (λ (y) y))),marks)))(λ (x) (λ (y) y))),marks))))][’error38

’error][x0‘(λ (,kont)(λ (,flag)(λ (,marks)(,kont ,x0 ))))])))(define (c-hat-cps e)(let ([k (gensym ’k)][f (gensym ’f)][m (gensym ’m)])‘(((,(c-cps e) (λ (x) x)) (λ (x) (λ (y) y))) (λ (x) ,(c-cps ’(λ (y) y))))))
7.4

Transformation testing

We can test that the property described by equation 6.2 holds for a given program p with(define (meaning-preserved? p)(alpha-eq? (eval λv (c-hat (eval λcm p))) (eval λv (c-hat p)))where alpha-eq? determines α-equivalence between two λ-calculus terms and eval is analias for the Redex native apply-reduction-relation∗.
Redex provides convenient functions to initiate random testing.
(redex-check λcm e (meaning-preserved? e))redex-check generates random terms according to the grammar of the given language(λcm) and category (e) in search of counterexamples to the predicate. It gradually increases
the size of the terms it generates, which we found useful in obtaining minimal test cases. We
subjected both the direct and CPS transformation to random testing and each eventually
withstood 10,000 random tests. Interestingly, no incorrect transformation withstood morethan 500 random tests before failing.

39

Chapter 8
Proof

The evaluation of a λcm program proceeds with the evolution of an evaluation context
and possibly reducible expression. When evaluation begins, the evaluation context is merely•, a placeholder for the eventual result, and the reducible expression, or redex, is the program
itself. The evaluation of arguments–both in application and continuation mark forms–defers
evaluation of the expression at hand by storing its evaluation context and evaluating subterms.
As these results are applied and evaluation continues, the size of the context fluctuates until
finally, if the program terminates, we are left with a single value to plug in •. This value isthe value of the program.
The state of evaluation at any given point can be encapsulated by a pair of anevaluation context E and an expression e which we write in unorthodox style as E[e]. In
order to prove that evaluation in the transformation corresponds to native evaluation, wemust relate this state with its corresponding transformation.
We do this by overloading Ccps to accommodate evaluation contexts which allows us
to formally relate E[e] and Ccps [E[e]]. We first define
Definition 19.

ξ(E) =




true

if E = E 0 [(wcm v 0 •)] for some E 0 and v 0false otherwise0
to denote the flags argument and assume that the marks argument is Ccps
[χ(E)]. We can

now define Ccps over contexts E ∈ λcm :40

Definition 20. Ccps [•](λ (value)
value)
Definition 21. Ccps [E [(• rand-value)]](λ (rator-value)(((Ccps [rand-expr ](λ (rand-value)0[χ(E)])))((((rator-value rand-value) Ccps [E ]) ξ(E)) Ccps
false)
0
Ccps [χ(E)]))
Definition 22. Ccps [E [(v0 •)]](λ (rand-value)0[χ(E)]))((((v0 rand-value) Ccps [E ]) ξ(E)) Ccps
Definition 23. Ccps [E [(wcm • body-expr )]](λ (mark-value)((λ (rest-marks)(((Ccps [body-expr ] Ccps [E ]) true) Cˆcps [((cons mark-value) rest-marks)]))0[χ(E)])))((ξ(E) Cˆcps [(snd χ(E))]) Ccps
Definition 24. Ccps [E [(wcm v0 •)]]
Ccps [E ]This allows us to define Ccps over a context-expression pair.
Definition 25. Ccps [E [e]]0(((Ccps [e] Ccps [E ]) ξ(E)) Ccps
[χ(E)])
0
From this definition, it is apparent that Cˆcps [p]=(((Ccps [p] Ccps [•]) ξ(•)) Ccps[•])=Ccps [•[p]].

Now we show that substitution is preserved by the transformation.
Lemma 1 (Substitution). For all e, x, v ∈ λcm , C[e[x ← v]] = C[e][x ← C 0 [v]].

41See appendix A for proof.
Finally, we define “filling the hole”, the insertion of a value in the context from which
it came.
Definition 26. Ccps [E [v ]]0(Ccps [E ] Ccps[v ])With each significant step of native evaluation formally related with the transformation,
we can express a simulation lemma.
Lemma 2 (Simulation). For all contexts E ∈ λcm and expressions e ∈ λcm , E[e] →λcm
E 0 [e0 ] =⇒ Ccps [E[e]] →∗λv Ccps [E 0 [e0 ]]We will reason by structural induction on both contexts E and terms e. Instead of
nesting the induction, which requires the consideration of |E| · |e| cases, we will take first
E and then e in isolation, in each assuming the correctness of the other, which requires theconsideration of only |E| + |e| cases.
First, we prove it holds for terms e. In each case, let E be an arbitrary context.
Proof. Case e = (e0 e1 ) By steps app1-app3, Ccps [E[(e0 e1 )]] →∗λv Ccps [E[(• e1 )][e0 ]].
Proof. Case e = (wcm e0 e1 ) By steps wcm1-wcm3, Ccps [E[(wcm e0 e1 )]] →∗λv Ccps [E[(wcm •e1 )][e0 ]].
Proof. Case e = (ccm) By steps ccm1-ccm3, Ccps [E[(ccm)]] →∗λv Ccps [E[χ(E)]].
Proof. Case e = v0 By steps value1-value3, Ccps [E[v0 ]] →∗λv Ccps [E[v0 ]].
Proof. Case e = x By steps x1-x4, Ccps [E[x]] →∗λv Ccps [E[error]].
Now, we prove it holds for contexts E. In each case, let v0 be an arbitrary value.
Proof. Case E = • This is identical to the case that e = v0 .
Proof. Case E = E 0 [(• e1 )] By step app4, Ccps [E[v0 ]] →λv Ccps [E 0 [(v0 •)][e1 ]].
42

Proof. Case E = E 0 [(v0 •)] By step app5, Ccps [E[v0 ]] →λv Ccps [E 0 [(v0 v1 )]].
By step app6 and lemma 1, Ccps [E 0 [(v0 v1 )]] →λv Ccps [E 0 [e0 ]].
Proof. Case E = E 0 [(wcm • e1 )] If E 0 = E 00 [(wcm v 0 •) for some E 00 and v 0 , then Ccps [E 0 [(wcm •e1 )][v0 ]] →∗λv Ccps [E 00 [(wcm v0 •)][e1 ]] by steps wcm4tail-wcm6tail.
Otherwise, Ccps [E 0 [(wcm • e1 )][v0 ]] →∗λv Ccps [E 0 [(wcm v0 •)][e1 ]] by steps wcm4nontailwcm6nontail.
Proof. Case E = E 0 [(wcm v0 •)] By definition, Ccps [E[v1 ]] = Ccps [E 0 [v1 ]].
0
Lemma 3. For all contexts E and terms e ∈ λcm , if E[e] →∗λcm v, then Ccps [E[e]] →∗λv Ccps[v].

Proof. If E[e] →∗λcm v, then E[e] →∗λcm •[v] →λcm v.
By simulation, E[e] →∗λcm •[v] =⇒ Ccps [E[e]] →∗λv Ccps [•[v]].
00
By definition, Ccps [•[v]] = (((Ccps [v] Ccps [•]) ξ(•)) Ccps
[χ(•)]) →∗λv Ccps[v], which is what

we sought.
ˆ For all programs p ∈ λcm , Cˆcps [evalcm (p)] ≡ evalv (Cˆcps [p]).
Correctness of C.
Proof.

p →∗λcm v =⇒ evalcm (p) = v

by definition of evalcm

0∗ˆ=⇒ C[evalcm (p)] →λv C [v]0ˆ=⇒ C[evalcm (p)] ≡ C [v]by definition of Cˆ
by definition of equivalency43

p →∗λcm v =⇒ •[p] →∗λcm v(since p →λcm •[p])=⇒ C[•[p]] →∗λv C 0 [v](by lemma 3)=⇒ (((C[p] C[•]) ξ(•)) C 0 [χ(•)]) →∗λv C[v]by definition of Cˆ(by definition of C)ˆ →∗λ C[v]=⇒ C[p]v
ˆ=⇒ evalv (C[p])= C 0 [v](by definition of evalv )Therefore, C[evalcm (p)] ≡ evalv (C[p]).

44Chapter 9
Conclusion

Continuation marks support a bevy of instrumentation tools and advanced language
features in a generalized, portable way. Despite their demonstrated utility, they have not yet
found their way into most languages. A verified characterization of continuation marks ina pure computational language provides implementors of higher-order languages a correctcompiler for continuation marks which we have demonstrated for JavaScript.
Our macro-style approach would be more useful if deployed as a proper macro, but
this requires a hygienic macro system which many languages lack. sweet.js is just such asystem for JavaScript in early stages and is ideal for our transformation.
Although we used some level of mechanization in the proof of the theorem, a formal proof assistant, such as Coq [3], would increase confidence out of the gate that thetransformation was correct.

45

References[1] A.W. Appel. Compiling with Continuations. Cambridge University Press, 2007.
[2] H.P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North Holland, 1984.
[3] B. Barras, S. Boutin, C. Cornes, J. Courant, J.C. Filliatre, E. Gimenez, H. Herbelin,
G. Huet, C. Munoz, C. Murthy, et al. The Coq Proof Assistant Reference Manual:
Version 6.1. 1997.
[4] J. Clements. Portable and High-Level Access to the Stack with Continuation Marks. PhD
thesis, Northeastern University Boston, 2006.
[5] J. Clements and M. Felleisen. A tail-recursive machine with stack inspection. Transactions
on Programming Languages and Systems, 26(6):1029–1052, 2004.
[6] J. Clements, M. Flatt, and M. Felleisen. Modeling an algebraic stepper. In Proceedings ofthe 10th European Symposium on Programming Languages and Systems, pages 320–334.
Springer, 2001.
[7] J. Clements, A. Sundaram, and D. Herman. Implementing continuation marks injavascript. In Proceedings of the Workshop on Scheme and Functional Programming,
pages 45–55. ACM, 2008.
[8] R.B. Findler and C. Klein. Redex: Practical Semantics Engineering. MIT Press, 2010.
[9] M.J. Fischer. Lambda calculus schemata. In Proceedings of the ACM Conference on
Proving Assertions About Programs, volume 6, pages 104–109. ACM, 1972.
[10] Matthew Flatt and PLT. Reference: Racket. Technical Report PLT-TR-2010-1, PLT
Inc., 2010. http://racket-lang.org/tr1/.
[11] C. Klein, J. Clements, C. Dimoulas, C. Eastlund, M. Felleisen, M. Flatt, J.A. McCarthy,
J. Rafkind, S. Tobin-Hochstadt, and R.B. Findler. Run your research: on the effectivenessof lightweight mechanization. In Proceedings of the 39th Annual Symposium on Principles
of Programming Languages, pages 285–296. ACM, 2012.

46

[12] E. Moggi. Computational lambda-calculus and monads. In Proceedings of the 4th Annual
Symposium on Logic in Computer Science, pages 14–23. IEEE, 1989.
[13] G. Pettyjohn, J. Clements, J. Marshall, S. Krishnamurthi, and M. Felleisen. Continuations
from generalized stack inspection. In ACM SIGPLAN Notices, volume 40, pages 216–227.
ACM, 2005.
[14] G.D. Plotkin. Call-by-name, call-by-value and the λ-calculus. Theoretical Computer
Science, 1(2):125–159, 1975.
[15] A.A. Sabry. The Formal Relationship Between Direct and Continuation-Passing Style
Optimizing Compilers: A Synthesis of Two Paradigms. PhD thesis, Rice University,
1994.
[16] D.B. Tucker and S. Krishnamurthi. Pointcuts and advice in higher-order languages. In
Proceedings of the 2nd International Conference on Aspect-Oriented Software Development, pages 158–167. ACM, 2003.
[17] D.S. Wallach, A.W. Appel, and E.W. Felten. Safkasi: a security mechanism for languagebased systems. Transactions on Software Engineering and Methodology, 9(4):341–378,
2000.

47

Appendix A
Proof of Lemma 1
A.1

Application Form

Proof. Case e = (rator-expr rand-expr )First, we have on the left side
Ccps [(rator-expr rand-expr )[x ← v ]] = Ccps [(rator-expr [x ← v ] rand-expr [x ← v ])]We have on the right side0[v ]]Ccps [(rator-expr rand-expr )][x ← Ccps

which, expanded, follows this sequence of equivalences:(λ (kont)(λ (flag)(λ (marks)(((Ccps [rator-expr ](λ (rator-value)(((Ccps [rand-expr ](λ (rand-value)((((rator-value rand-value) kont) flag) marks)))
false) marks)))
0
false) marks))))[x ← Ccps[v ]](λ (kont)(λ (flag)(λ (marks)(((Ccps [rator-expr ](λ (rator-value)(((Ccps [rand-expr ](λ (rand-value)((((rator-value rand-value) kont) flag) marks)))
false) marks)))
0
false) marks))[x ← Ccps[v ]]))48

(λ (kont)(λ (flag)(λ (marks)(((Ccps [rator-expr ](λ (rator-value)(((Ccps [rand-expr ](λ (rand-value)((((rator-value rand-value) kont) flag) marks)))
false) marks)))
0[v ]])))
false) marks)[x ← Ccps
(λ (kont)(λ (flag)(λ (marks)(((Ccps [rator-expr ](λ (rator-value)(((Ccps [rand-expr ](λ (rand-value)((((rator-value rand-value) kont) flag) marks)))
false) marks)))00[v ]]))))[v ]] marks[x ← Ccps
false)[x ← Ccps
(λ (kont)(λ (flag)(λ (marks)(((Ccps [rator-expr ](λ (rator-value)(((Ccps [rand-expr ](λ (rand-value)((((rator-value rand-value) kont) flag) marks)))0[v ]]false) marks)))[x ← Ccps
0false[x ← Ccps [v ]]) marks))))(λ (kont)(λ (flag)(λ (marks)
0(((Ccps [rator-expr ][x ← Ccps[v ]](λ (rator-value)(((Ccps [rand-expr ](λ (rand-value)((((rator-value rand-value) kont) flag) marks)))
0
false) marks))[x ← Ccps[v ]])
false) marks))))49

(λ (kont)(λ (flag)(λ (marks)0[v ]](((Ccps [rator-expr ][x ← Ccps
(λ (rator-value)(((Ccps [rand-expr ](λ (rand-value)((((rator-value rand-value) kont) flag) marks)))
0[v ]]))
false) marks)[x ← Ccps
false) marks))))(λ (kont)(λ (flag)(λ (marks)0[v ]](((Ccps [rator-expr ][x ← Ccps
(λ (rator-value)(((Ccps [rand-expr ](λ (rand-value)((((rator-value rand-value) kont) flag) marks)))00[v ]])))[v ]] marks[x ← Ccps
false)[x ← Ccps
false) marks))))(λ (kont)(λ (flag)(λ (marks)
0(((Ccps [rator-expr ][x ← Ccps[v ]](λ (rator-value)(((Ccps [rand-expr ](λ (rand-value)0[v ]]((((rator-value rand-value) kont) flag) marks)))[x ← Ccps
0false[x ← Ccps [v ]]) marks)))
false) marks))))(λ (kont)(λ (flag)(λ (marks)
0(((Ccps [rator-expr ][x ← Ccps[v ]](λ (rator-value)0(((Ccps [rand-expr ][x ← Ccps[v ]](λ (rand-value)0((((rator-value rand-value) kont) flag) marks))[x ← Ccps[v ]])
false) marks)))
false) marks))))50

(λ (kont)(λ (flag)(λ (marks)0[v ]](((Ccps [rator-expr ][x ← Ccps
(λ (rator-value)0(((Ccps [rand-expr ][x ← Ccps[v ]](λ (rand-value)0((((rator-value rand-value) kont) flag) marks)[x ← Ccps[v ]]))
false) marks)))
false) marks))))(λ (kont)(λ (flag)(λ (marks)0[v ]](((Ccps [rator-expr ][x ← Ccps
(λ (rator-value)0[v ]](((Ccps [rand-expr ][x ← Ccps
(λ (rand-value)00((((rator-value rand-value) kont) flag)[x ← Ccps[v ]] marks[x ← Ccps[v ]])))
false) marks)))
false) marks))))(λ (kont)(λ (flag)(λ (marks)
0(((Ccps [rator-expr ][x ← Ccps[v ]](λ (rator-value)0(((Ccps [rand-expr ][x ← Ccps[v ]](λ (rand-value)00[v ]]) marks)))[v ]] flag[x ← Ccps((((rator-value rand-value) kont)[x ← Ccps
false) marks)))
false) marks))))(λ (kont)(λ (flag)(λ (marks)
0(((Ccps [rator-expr ][x ← Ccps[v ]](λ (rator-value)0(((Ccps [rand-expr ][x ← Ccps[v ]](λ (rand-value)00((((rator-value rand-value)[x ← Ccps[v ]] kont[x ← Ccps[v ]]) flag) marks)))
false) marks)))
false) marks))))51

(λ (kont)(λ (flag)(λ (marks)0[v ]](((Ccps [rator-expr ][x ← Ccps
(λ (rator-value)0(((Ccps [rand-expr ][x ← Ccps[v ]](λ (rand-value)00((((rator-value[x ← Ccps[v ]] rand-value[x ← Ccps[v ]]) kont) flag) marks)))
false) marks)))
false) marks))))(λ (kont)(λ (flag)(λ (marks)0[v ]](((Ccps [rator-expr ][x ← Ccps
(λ (rator-value)0[v ]](((Ccps [rand-expr ][x ← Ccps
(λ (rand-value)((((rator-value rand-value) kont) flag) marks)))
false) marks)))
false) marks))))And finally, by induction, we have(λ (kont)(λ (flag)(λ (marks)(((Ccps [rator-expr [x ← v ]](λ (rator-value)(((Ccps [rand-expr [x ← v ]](λ (rand-value)((((rator-value rand-value) kont) flag) marks)))
false) marks)))
false) marks))))which is equal to
Ccps [(rator-expr [x ← v ] rand-expr [x ← v ])]Therefore,
0
Ccps [(rator-expr rand-expr )[x ← v ]] = Ccps [(rator-expr rand-expr )][x ← Ccps
[v ]]

52

A.2

wcm Form

Proof. Case e = (wcm mark-expr body-expr )First, we have on the left side
Ccps [(wcm mark-expr body-expr )[x ← v ]] = Ccps [(wcm mark-expr [x ← v ] body-expr [x ← v ])]We have on the right side0
Ccps [(wcm mark-expr body-expr )][x ← Ccps[v ]]which, expanded, follows this sequence of equivalences:(λ (kont)(λ (flag)(λ (marks)(((Ccps [mark-expr ](λ (mark-value)((λ (rest-marks)(((Ccps [body-expr ] kont) true) Cˆcps [((cons mark-value) rest-marks)]))((flag Cˆcps [(snd marks)]) marks))))0false) marks))))[x ← Ccps[v ]](λ (kont)(λ (flag)(λ (marks)(((Ccps [mark-expr ](λ (mark-value)((λ (rest-marks)(((Ccps [body-expr ] kont) true) Cˆcps [((cons mark-value) rest-marks)]))((flag Cˆcps [(snd marks)]) marks))))0false) marks)))[x ← Ccps[v ]])(λ (kont)(λ (flag)(λ (marks)(((Ccps [mark-expr ](λ (mark-value)((λ (rest-marks)(((Ccps [body-expr ] kont) true) Cˆcps [((cons mark-value) rest-marks)]))((flag Cˆcps [(snd marks)]) marks))))0false) marks))[x ← Ccps[v ]]))(λ (kont)(λ (flag)53

(λ (marks)(((Ccps [mark-expr ](λ (mark-value)((λ (rest-marks)(((Ccps [body-expr ] kont) true) Cˆcps [((cons mark-value) rest-marks)]))((flag Cˆcps [(snd marks)]) marks))))0[v ]])))
false) marks)[x ← Ccps
(λ (kont)(λ (flag)(λ (marks)(((Ccps [mark-expr ](λ (mark-value)((λ (rest-marks)(((Ccps [body-expr ] kont) true) Cˆcps [((cons mark-value) rest-marks)]))((flag Cˆcps [(snd marks)]) marks))))00[v ]]))))[v ]] marks[x ← Ccps
false)[x ← Ccps
(λ (kont)(λ (flag)(λ (marks)(((Ccps [mark-expr ](λ (mark-value)((λ (rest-marks)(((Ccps [body-expr ] kont) true) Cˆcps [((cons mark-value) rest-marks)]))0((flag Cˆcps [(snd marks)]) marks))))[x ← Ccps[v ]]0false[x ← Ccps [v ]]) marks))))(λ (kont)(λ (flag)(λ (marks)
0(((Ccps [mark-expr ][x ← Ccps[v ]](λ (mark-value)((λ (rest-marks)(((Ccps [body-expr ] kont) true) Cˆcps [((cons mark-value) rest-marks)]))0((flag Cˆcps [(snd marks)]) marks)))[x ← Ccps[v ]])
false) marks))))(λ (kont)(λ (flag)(λ (marks)
0(((Ccps [mark-expr ][x ← Ccps[v ]](λ (mark-value)54

((λ (rest-marks)(((Ccps [body-expr ] kont) true) Cˆcps [((cons mark-value) rest-marks)]))0((flag Cˆcps [(snd marks)]) marks))[x ← Ccps[v ]]))
false) marks))))(λ (kont)(λ (flag)(λ (marks)0[v ]](((Ccps [mark-expr ][x ← Ccps
(λ (mark-value)((λ (rest-marks)
0(((Ccps [body-expr ] kont) true) Cˆcps [((cons mark-value) rest-marks)]))[x ← Ccps
[v ]]
0
ˆ
((flag Ccps [(snd marks)]) marks)[x ← Ccps [v ]])))
false) marks))))(λ (kont)(λ (flag)(λ (marks)
0(((Ccps [mark-expr ][x ← Ccps[v ]](λ (mark-value)((λ (rest-marks)
0[v ]])(((Ccps [body-expr ] kont) true) Cˆcps [((cons mark-value) rest-marks)])[x ← Ccps00((flag Cˆcps [(snd marks)])[x ← Ccps [v ]] marks[x ← Ccps [v ]]))))
false) marks))))(λ (kont)(λ (flag)(λ (marks)0[v ]](((Ccps [mark-expr ][x ← Ccps
(λ (mark-value)((λ (rest-marks)
00(((Ccps [body-expr ] kont) true)[x ← Ccps[v ]] Cˆcps [((cons mark-value) rest-marks)][x ← Ccps[00
ˆ((flag[x ← Ccps [v ]] Ccps [(snd marks)][x ← Ccps [v ]]) marks))))false) marks))))(λ (kont)(λ (flag)(λ (marks)
0(((Ccps [mark-expr ][x ← Ccps[v ]](λ (mark-value)((λ (rest-marks)
00(((Ccps [body-expr ] kont)[x ← Ccps[v ]] true[x ← Ccps[v ]]) Cˆcps [((cons mark-value) rest-marks((flag Cˆcps [(snd marks)]) marks))))55

false) marks))))(λ (kont)(λ (flag)(λ (marks)0[v ]](((Ccps [mark-expr ][x ← Ccps
(λ (mark-value)((λ (rest-marks)
00(((Ccps [body-expr ][x ← Ccps[v ]] kont[x ← Ccps[v ]]) true) Cˆcps [((cons mark-value) rest-marks((flag Cˆcps [(snd marks)]) marks))))false) marks))))(λ (kont)(λ (flag)(λ (marks)0[v ]](((Ccps [mark-expr ][x ← Ccps
(λ (mark-value)((λ (rest-marks)
0(((Ccps [body-expr ][x ← Ccps[v ]] kont) true) Cˆcps [((cons mark-value) rest-marks)]))((flag Cˆcps [(snd marks)]) marks))))false) marks))))And finally, by induction, we have(λ (kont)(λ (flag)(λ (marks)(((Ccps [mark-expr [x ← v ]](λ (mark-value)((λ (rest-marks)(((Ccps [body-expr [x ← v ]] kont) true) Cˆcps [((cons mark-value) rest-marks)]))((flag Cˆcps [(snd marks)]) marks))))false) marks))))which is equal to
Ccps [(wcm mark-expr [x ← v ] body-expr [x ← v ])]Therefore,
0
Ccps [(wcm mark-expr body-expr )[x ← v ]] = Ccps [(wcm mark-expr body-expr )][x ← Ccps
[v ]]

56

A.3

ccm Form

Proof. Case e=(ccm)First, we have on the left side
Ccps [(ccm)[x ← v ]] = Ccps [(ccm)]
We have on the right side0
Ccps [(ccm)][x ← Ccps[v ]]which, expanded, follows this sequence of equivalences:(λ (kont)(λ (flag)(λ (marks)
0[v ]](kont marks))))[x ← Ccps
(λ (kont)(λ (flag)(λ (marks)
0(kont marks)))[x ← Ccps[v ]])(λ (kont)(λ (flag)(λ (marks)
0(kont marks))[x ← Ccps[v ]]))(λ (kont)(λ (flag)(λ (marks)
0(kont marks)[x ← Ccps[v ]])))(λ (kont)(λ (flag)(λ (marks)
00[v ]] marks[x ← Ccps[v ]]))))(kont[x ← Ccps
(λ (kont)(λ (flag)(λ (marks)(kont marks))))which is equal to
Ccps [(ccm)]
57

0Therefore, Ccps [(ccm)[x ← v ]]=Ccps[(ccm)][x ← Ccps[v ]].

A.4

Value Form

Proof. Case e = (λ (x ) e0 )On the left side, we haveCcps [(λ (x ) e0 )[x ← v ]] = Ccps [(λ (x ) e0 )]On the right side, we have0[v ]]Ccps [(λ (x ) e0 )][x ← Ccps

which follows(λ (kont)(λ (flag)(λ (marks)
0[v ]](kont (λ (x ) Ccps [e0 ])))))[x ← Ccps
(λ (kont)(λ (flag)(λ (marks)
0(kont (λ (x ) Ccps [e0 ]))))[x ← Ccps[v ]])(λ (kont)(λ (flag)(λ (marks)
0[v ]]))(kont (λ (x ) Ccps [e0 ])))[x ← Ccps
(λ (kont)(λ (flag)(λ (marks)
0(kont (λ (x ) Ccps [e0 ]))[x ← Ccps[v ]])))(λ (kont)(λ (flag)(λ (marks)
00(kont[x ← Ccps[v ]] (λ (x ) Ccps [e0 ])[x ← Ccps[v ]]))))(λ (kont)(λ (flag)(λ (marks)(kont (λ (x ) Ccps [e0 ])))))
58

Ccps [(λ (x ) e0 )]0[v ]].
Therefore, Ccps [(λ (x ) e0 )[x ← v ]] = Ccps [(λ (x ) e0 )][x ← Ccps

Proof. Case e = (λ (x0 ) e0 ) where x0 6= x
On the left side, we haveCcps [(λ (x0 ) e0 )[x ← v ]] = Ccps [(λ (x0 ) e0 )]On the right side, we have0[v ]]Ccps [(λ (x0 ) e0 )][x ← Ccps

which follows(λ (kont)(λ (flag)(λ (marks)
0(kont (λ (x0 ) Ccps [e0 ])))))[x ← Ccps[v ]](λ (kont)(λ (flag)(λ (marks)
0[v ]])(kont (λ (x0 ) Ccps [e0 ]))))[x ← Ccps
(λ (kont)(λ (flag)(λ (marks)
0[v ]]))(kont (λ (x0 ) Ccps [e0 ])))[x ← Ccps
(λ (kont)(λ (flag)(λ (marks)
0(kont (λ (x0 ) Ccps [e0 ]))[x ← Ccps[v ]])))(λ (kont)(λ (flag)(λ (marks)
00(kont[x ← Ccps[v ]] (λ (x0 ) Ccps [e0 ])[x ← Ccps[v ]]))))(λ (kont)(λ (flag)(λ (marks)
0(kont (λ (x0 ) Ccps [e0 ][x ← Ccps[v ]])))))

59

By induction, this is(λ (kont)(λ (flag)(λ (marks)(kont (λ (x0 ) Ccps [e0 [x ← v ]])))))
which equals
Ccps [(λ (x0 ) e0 [x ← v ])]0[v ]].
Therefore, Ccps [(λ (x0 ) e0 )[x ← v ]] = Ccps [(λ (x0 ) e0 )][x ← Ccps

A.5

Variable Form

Proof. Case e = x
On the left, we have Ccps [x [x ← v ]] = Ccps [v ].
0[v ]] which follows
On the right, we have Ccps [x ][x ← Ccps
(λ (kont)(λ (flag)(λ (marks)
0[v ]](kont x ))))[x ← Ccps
(λ (kont)(λ (flag)(λ (marks)
0[v ]])(kont x )))[x ← Ccps
(λ (kont)(λ (flag)(λ (marks)
0(kont x ))[x ← Ccps[v ]]))(λ (kont)(λ (flag)(λ (marks)
0(kont x )[x ← Ccps[v ]])))(λ (kont)(λ (flag)(λ (marks)
00(kont[x ← Ccps[v ]] x [x ← Ccps[v ]]))))60

(λ (kont)(λ (flag)(λ (marks)
0[v ]))))(kont Ccps
Ccps [v ]0
Therefore, Ccps [x [x ← v ]] = Ccps [x ][x ← Ccps[v ]].

Proof. Case e = x0 where x0 6= x
On the left, we have Ccps [x0 [x ← v ]]=Ccps [x0 ].
0[v ]], which follows
On the right, we have Ccps [x0 ][x ← Ccps
(λ (kont)(λ (flag)(λ (marks)
0(kont x0 ))))[x ← Ccps[v ]](λ (kont)(λ (flag)(λ (marks)
0[v ]])(kont x0 )))[x ← Ccps
(λ (kont)(λ (flag)(λ (marks)
0[v ]]))(kont x0 ))[x ← Ccps
(λ (kont)(λ (flag)(λ (marks)
0(kont x0 )[x ← Ccps[v ]])))(λ (kont)(λ (flag)(λ (marks)
00(kont[x ← Ccps[v ]] x0 [x ← Ccps[v ]]))))(λ (kont)(λ (flag)(λ (marks)(kont x0 ))))

61

Ccps [x0 ]0[v ].
Therefore, Ccps [x0 [x ← v ]] = Ccps [x0 ][x ← Ccps

62

Appendix B
Reductions
B.1

Application Form

Ccps [E [(rator-expr rand-expr )]]((((λ (kont)(λ (flag)(λ (marks)(((Ccps [rator-expr ](λ (rator-value)(((Ccps [rand-expr ](λ (rand-value)((((rator-value rand-value) kont) flag) marks)))
false) marks)))
false) marks))))0[χ(E)])
C[E]) ξ(E)) Ccps
app1(((λ (flag)(λ (marks)(((Ccps [rator-expr ](λ (rator-value)(((Ccps [rand-expr ](λ (rand-value)((((rator-value rand-value) C[E]) flag) marks)))
false) marks)))
false) marks)))0ξ(E)) Ccps
[χ(E)])app2((λ (marks)(((Ccps [rator-expr ](λ (rator-value)(((Ccps [rand-expr ](λ (rand-value)((((rator-value rand-value) C[E]) ξ(E)) marks)))
63

false) marks)))
0
false) marks)) Ccps
[χ(E)])
app3(((Ccps [rator-expr ](λ (rator-value)(((Ccps [rand-expr ](λ (rand-value)0((((rator-value rand-value) C[E]) ξ(E)) Ccps
[χ(E)])))
0false) Ccps [χ(E)])))
0false) Ccps [χ(E)])
app4(((Ccps [rand-expr ](λ (rand-value)
00((((Ccps[v0 ] rand-value) C[E]) ξ(E)) Ccps
[χ(E)])))
0false) Ccps [χ(E)])
app5
0
0
0
[χ(E)])[v1 ]) C[E]) ξ(E)) Ccps[v0 ] Ccps((((Ccps000((((Ccps[(λ (x ) e0 )] Ccps
[v1 ]) C[E]) ξ(E)) Ccps
[χ(E)])

app6
00[χ(E)])[v1 ]] C[E]) ξ(E)) Ccps(((Ccps [e0 ][x ← Ccps

B.2

wcm form

Ccps [E [(wcm mark-expr body-expr )]]((((λ (kont)(λ (flag)(λ (marks)(((Ccps [mark-expr ](λ (mark-value)((λ (rest-marks)
0(((Ccps [body-expr ] kont) true) Ccps[((cons mark-value) rest-marks)]))ˆ((flag Ccps [(snd marks)]) marks))))false) marks))))0C[E]) ξ(E)) Ccps
[χ(E)])
wcm1(((λ (flag)64

(λ (marks)(((Ccps [mark-expr ](λ (mark-value)((λ (rest-marks)
0(((Ccps [body-expr ] C[E]) true) Ccps[((cons mark-value) rest-marks)]))ˆ((flag Ccps [(snd marks)]) marks))))false) marks)))0[χ(E)])
ξ(E)) Ccps
wcm2((λ (marks)(((Ccps [mark-expr ](λ (mark-value)((λ (rest-marks)
0(((Ccps [body-expr ] C[E]) true) Ccps[((cons mark-value) rest-marks)]))ˆ((ξ(E) Ccps [(snd marks)]) marks))))false) marks))0[χ(E)])
Ccps
wcm3(((Ccps [mark-expr ](λ (mark-value)((λ (rest-marks)
0[((cons mark-value) rest-marks)]))(((Ccps [body-expr ] C[E]) true) Ccps0ˆ((ξ(E) Ccps [(snd χ(E))]) Ccps [χ(E)]))))
0false) Ccps
[χ(E)])
wcm4tail((λ (rest-marks)
0[((cons mark-value) rest-marks)]))(((Ccps [body-expr ] C[E]) true) Ccps
0((true Cˆcps [(snd χ(E))]) Ccps [χ(E)]))
wcm5tail((λ (rest-marks)
0(((Ccps [body-expr ] C[E]) true) Ccps[((cons mark-value) rest-marks)]))0
Ccps [(snd χ(E))])
wcm6tail0(((Ccps [body-expr ] C[E]) true) Ccps[((cons mark-value) (snd χ(E)))])

wcm4nontail((λ (rest-marks)
650(((Ccps [body-expr ] C[E]) true) Ccps[((cons mark-value) rest-marks)]))0[χ(E)]))((false Cˆcps [(snd χ(E))]) Ccps

wcm5nontail((λ (rest-marks)
0(((Ccps [body-expr ] C[E]) true) Ccps[((cons mark-value) rest-marks)]))0
Ccps [χ(E)])
wcm6nontail
0(((Ccps [body-expr ] C[E]) true) Ccps[((cons mark-value) χ(E))])

B.3

ccm form

Ccps [E [(ccm)]]((((λ (kont)(λ (flag)(λ (marks)(kont marks))))0C[E]) ξ(E)) Ccps
[χ(E)])
ccm1(((λ (flag)(λ (marks)(C[E] marks)))0ξ(E)) Ccps
[χ(E)])ccm2((λ (marks)(C[E] marks))
0
Ccps [χ(E)])
ccm3
0(C[E] Ccps
[χ(E)])

B.4

Value Form

Ccps [E [v ]]=Ccps [E [(λ (x ) e)]]((((λ (kont)(λ (flag)(λ (marks)(kont (λ (x ) Ccps [e])))))
0C[E]) ξ(E)) Ccps
[χ(E)])
66

value1(((λ (flag)(λ (marks)(C[E] (λ (x ) Ccps [e]))))0ξ(E)) Ccps
[χ(E)])
value2((λ (marks)(C[E] (λ (x ) Ccps [e])))0
Ccps [χ(E)])
value3(C[E] (λ (x ) Ccps [e]))B.5

Variable Form

Ccps [E [x ]]((((λ (kont)(λ (flag)(λ (marks)(kont x ))))
0[χ(E)])
C[E]) ξ(E)) Ccps
x1(((λ (flag)(λ (marks)(C[E] x )))0[χ(E)])
ξ(E)) Ccpsx2((λ (marks)(C[E] x ))0
Ccps
[χ(E)])
x3(C[E] x )x4
(C[E] error)x5
error
67