Verifying CPS Transformations in Isabelle/HOL
Yasuhiko Minamide

Koji Okuma

University of Tsukuba
and
PRESTO, JST

University of Tsukuba

okuma@score.is.tsukuba.ac.jp

minamide@is.tsukuba.ac.jp

ABSTRACT
We have veriﬁed several versions of the CPS transformationin Isabelle/HOL. In our veriﬁcation we adopted ﬁrst-orderabstract syntax with variable names so that the formalization is close to that of hand-written proofs and compilers.
To simplify treatment of fresh variables introduced by thetransformation, we introduced abstract syntax parameterized with the type of variables. We also found that thestandard formalization of α-equivalence was cumbersome
for theorem provers and reformulated α-equivalence as asyntax-directed deductive system. To simplify veriﬁcationof the CPS transformation on the language extended with
let-expressions, it was essential to impose that variables are
uniquely used in a program.

Categories and Subject Descriptors
D.3.4 [Programming Languages]: Processors—compilers,optimization; F.1.1 [Mathematical Logic and Formal Languages]: Mathematical Logic—mechanical theorem proving

General Terms
Languages, Veriﬁcation

Keywords
Program transformation, theorem proving, correctness proofs

1. INTRODUCTION
Recently developed compilers apply various sophisticatedprogram transformations to achieve high performance andto implement various advanced features of programming languages. As transformations become more and more sophisticated, their hand-written correctness proofs become less andless reliable. Thus, it is desirable to verify the correctnessof program transformations with theorem provers.
We veriﬁed several versions of the CPS transformationin Isabelle/HOL. The CPS transformation has been used

Permission to make digital or hard copies of all or part of this work forpersonal or classroom use is granted without fee provided that copies are
not made or distributed for profit or commercial advantage and that copies
bear this notice and the full citation on the first page. To copy otherwise, torepublish, to post on servers or to redistribute to lists, requires prior specificpermission and/or a fee.
MERλIN’03, August 26, 2003, Uppsala, Sweden
Copyright 2003 ACM 1-58113-800-8/03/0008 ...$5.00.

in compilers of functional programming languages to makeexplicit the control ﬂow of a program and to implement
continuations as ﬁrst-class objects [17, 2]. The transformation translates programs into a special form called thecontinuation-passing style.
As a representation of lambda terms, we chose a ﬁrst-orderabstract syntax with variable names for the following reasons. It is simple and close to the representation of lambda
terms in hand-written proofs. Even if variable names areused in abstract syntax, there is no need to rename them forthe deﬁnition of reduction semantics, because we only consider the evaluation of closed programs and an expression
inside a lambda abstraction is not evaluated. Furthermore,
abstract syntax with variable names is very close to the intermediate languages used in compilers. Thus, veriﬁcation
based on abstract syntax with variable names may help theveriﬁcation of actual compilers in future research.
We veriﬁed several versions of the CPS transformation,
those of Plotkin [16], Danvy and Filinski [4], and Danvy
and Nielsen [5]. Plotkin’s transformation is simple, but introduces redundant redexes. The other two are optimized
transformations and it is more diﬃcult to show their correctness. We wrote our proof scripts in the proof language
Isabelle/Isar [19]. By using Isabelle/Isar we could write
human-readable structured proofs. The proof scripts of our
veriﬁcation can be obtained from http://www.score.is.
tsukuba.ac.jp/~minamide/cps/. There are several diﬃculties in our veriﬁcation related to variable names.
The ﬁrst problem relates to fresh variables introduced by
the transformation. All the CPS transformations introduce
some fresh variables, which must be diﬀerent from the variables occurring in an original term. This restriction must
be maintained explicitly: lemmas require explicit restrictions about variables. However, this makes it diﬃcult toprove them in Isabelle/HOL. To solve this problem, we introduced an abstract syntax parameterized with the type ofvariables. With this abstract syntax, it is possible to implicitly impose the restriction.
The second problem relates to the treatment of the αequivalence of lambda terms. Our veriﬁcation of Danvy
and Nielsen’s and Danvy and Filinski’s transformations relyon the α-equivalence of lambda terms. However, we foundthat the standard formalization of α-equivalence was cumbersome for theorem provers. Thus, we reformulated αequivalence as a syntax-directed deductive system.
The last problem is encountered in veriﬁcation of Danvy
and Nielsen’s transformation on the language extended with
let-expressions. For the veriﬁcation of this transformation,

we imposed that let-bound variables are uniquely used ina program. Without this restriction, formalization of thistransformation requires explicit renaming of let-bound variables and that makes veriﬁcation diﬃcult to conduct.
This paper is organized as follows. In Section 2 we introduce the language we consider and review the CPS transformation. We also explain why we choose an abstract syntax
with variable names. In Section 3 we present the veriﬁcationof Plotkin’s transformation and introduce a parameterized
abstract syntax. In Section 4 we present the veriﬁcation of
Danvy and Nielsen’s transformation. Our deductive systemof α-equivalence is discussed in this section. We also extend
our veriﬁcation to the language with let-expressions. In Section 5 we outline our formalization of Danvy and Filinksi’stransformation. Finally we review related work and present
our conclusions.

2. LANGUAGE AND TRANSFORMATION
We describe the syntax and semantics of the language
we will consider in this paper and review Plotkin’s CPS
transformation. We also clarify why we chose an abstract
syntax with variable names instead of an abstract syntax
based on de Bruijn indexes.
The syntax of the language we consider in this paper isdeﬁned as follows:
M ::= x | λx.M | M M
We consider a call-by-value operational semantics for thislanguage. The operational semantics of the language is deﬁned based on the following β-reduction rule.
(λx.M )V → M [V /x]
where V is a value, either a variable or an abstraction. We
consider only the evaluation of closed programs. Thus, forevaluation of programs, the substitution M [V /x] is required
only for closed V . By considering this restriction, the substitution M [N/x] is deﬁned without considering the renamingof bound variables as follows:
λx.M(if x = y)(λx.M )[N/y] =λx.(M [N/y]) (if x = y)This is well-deﬁned without considering the α-equivalenceof lambda terms, and thus the operational semantics ofthe language is also well-deﬁned without the α-equivalenceof lambda terms. This makes it possible to formalize theoperational semantics based on abstract syntax with variable names directly without problems of renaming. This is
the ﬁrst reason why we chose abstract syntax with variablenames.
CPS transformations have been used in compilers of functional programming languages to make explicit the control
ﬂow of a program and to implement continuation as ﬁrstclass objects [17, 2]. The transformation translates programs into a special form called the continuation-passing
style. The following is Plotkin’s transformation [16]:[[x]][[λx.M ]][[M N ]]

=
=
=

λk.kx
λk.k(λx.[[M ]])λk.[[M ]](λm.[[N ]](λn.mnk))

where k, m and n are fresh variables. The translated program is evaluated with the initial continuation λx.x. Plotkin

showed that M and [[M ]](λx.x) are evaluated to equivalentvalues.
The transformation is deﬁned by taking advantage of variable names. If we adopt an abstract syntax based on de Bruijn
indexes [6], we encounter diﬃculties in formalizing the transformation. Let us consider the following transformation ofx x by Plotkin’s CPS transformation.
[[x x]] = λk.(λk.kx)(λm.(λk.kx)(λn.mnk)))
The transformation of x does not depend on the contexts
where it appears. If we represent x by 0 of de Bruijn indexes,
the transformation is revised as follows:[[0 0]] = λ(λ 0 2)(λ(λ 0 3)(λ 1 0 2))
where the transformation of 0 is context-sensitive: (λ 0 2)or (λ 0 3). As a result, the CPS transformation of terms
represented by de Bruijn indexes is context-sensitive andseems to be more diﬃcult to manage. This is another reason
we chose an abstract syntax with variable names. We thinkthat de Bruijn indexes are not suitable for the formalizationof many program transformations because they are often
deﬁned by taking advantage of variable names.

2.1

Language and Semantics in Isabelle/HOL

We review Isabelle/HOL and show how we formalized thelanguage and operational semantics based on abstract syntax with variable names. Isabelle is a generic interactive
theorem prover that can be instantiated with several diﬀerent object logics [13] and Isabelle/HOL is an instantiationof Isabelle to Church’s higher-order logic [12]. We refer toIsabelle/HOL as Isabelle in the rest of this paper. The typesystem of Isabelle is similar to that of ML and has ML-stylepolymorphic types. Types follow the syntax of ML-types
except that the function arrow is =>.
As discussed earlier, we chose ﬁrst-order abstract syntax with variable names as the representation of lambda
terms. The abstract syntax of lambda terms is deﬁned by
the datatype deﬁnition as follows:
datatype lt = Var nat| Abs nat lt| "$" lt lt (infixl 200)
where variable names are represented by natural numbers:
nat. The keyword infixl means that the operator $ canbe used in inﬁx notation with priority 200. For example,
λx.λy.xy is represented by the following term in Isabelle.
Abs 0 (Abs 1 (Var 0 $ Var 1))
This representation of terms is almost the same as those ofintermediate languages of most compilers.
The observation in the previous section simpliﬁes the formalization of substitution and reduction. Substitution isdeﬁned as a primitive recursive function in Isabelle as follows:
primrec(Var y)[V/x] = (if y = x then V else Var y)(Abs y M)[V/x] = (if (y = x) then Abs y M
else Abs y (M[V/x]))(M $ N)[V/x] = M[V/x] $ N[V/x]
Since the substitution M[V/x] is applied only to a closed
term V, there is no need to rename variable y in the deﬁnition
for abstraction. With substitution the reduction relation isdeﬁned as an inductively-deﬁned relation.

consts CPS :: lt => lt ("([ ])" [250] 250)
primrec([Var x]) = Abs 0 (Var 0 $ Var x)([Abs x M]) = Abs 0 (Var 0 $ Abs x ([M]))([M $ N]) = Abs 0 (([M]) $ (Abs 1 (([N]) $ (Abs 2 (Var 1 $ Var 2 $ Var 0)))))
Figure 1: Plotkin’s CPS transformation: naive formalization
consts CPS :: ’a lt => ’a variable lt ("([ ])" [250] 250)
primrec([Var x]) = Abs k (Var k $ Var (x~))([Abs x M]) = Abs k (Var k $ (Abs (x~) ([M]) ))([M $ N]) = Abs k (([M]) $ (Abs m (([N]) $ (Abs n (Var m $ Var n $ Var k)))))
Figure 2: Plotkin’s CPS transformation: revised formalization.
constseval :: (lt * lt) set
inductive evalintros[[isValue V; closed V]] ⇒((Abs x M) $ V, M[V/x])∈eval[[isValue V; (M,M’)∈eval]] ⇒ (V $ M, V $ M’)∈eval(M,M’)∈eval ⇒ (M $ N, M’ $ N)∈eval

The type of terms ’a lt is parameterized with the type ’aof variables. The type ’a can be any type: our deﬁnitionof substitution does not require renaming and thus a typewith a ﬁnite number of values can be used for variables.
In this representation, the source and target languages
with diﬀerent sets of variables can share the same abstract
syntax. In the CPS transformation, we represent the set ofvariables of the target language by the following datatype.

This deﬁnition introduces a relation eval between lt. To
ensure that substitution is applied only if V is closed, the rule
for the β-axiom is restricted to the case where V is closed.

datatype ’a variable = Orig ’a ("_~")| k | m | n

3. PLOTKIN’S CPS TRANSFORMATION
We outline our veriﬁcation of Plotkin’s CPS transformation in this section. The key to our veriﬁcation is to introduce abstract syntax parameterized with the type of variables. The parameterized abstract syntax is implemented asa polymorphic datatype.
Plotkin’s transformation can be formalized as a primitive
recursive function in Isabelle if we ﬁx the representation of
the variables k, m and n to some natural numbers. Figure 1 shows a formalization of the transformation where k,m and n are represented by the natural numbers 0, 1 and 2,
respectively. The notation ([M]) is introduced for (CPS M) 1 .
We ﬁrst attempted to verify the correctness of the transformation based on this formalization, but found that theformalization was cumbersome for veriﬁcation. The transformation is valid only if the variables represented by 0, 1
and 2 do not occur in a program. This condition must be
maintained in every lemma, which makes it diﬃcult to provelemmas, especially with automated theorem-proving tactics.
This problem occurs because the distinction between thevariables in an original term and those introduced by thetransformation is not clear from the formalization. To overcome this problem we introduce an abstract syntax parameterized with the set of variables. The abstract syntax is
implemented by the following polymorphic datatype deﬁnition.
datatype ’a lt = Var ’a| Abs ’a "’a lt"| $ "’a lt" "’a lt" (infixl 200)1
We use notation ([M]) instead of [[M]] because [[M]] conﬂicts
with Isabelle’s notation.

The variables introduced by the transformation are represented by constants: k, m and n. A variable x in the source
language is translated into x~, that is, an abbreviation of
Orig x.
Using this abstract syntax, the CPS transformation is deﬁned as a polymorphic primitive recursive function. The
transformation can then be obtained by reﬁning the previous deﬁnition and is shown in Figure 2. By this formalization, freshness of the variables k, m and n is imposed
implicitly and we do not have to maintain the restriction
explicitly. Then, proofs of many lemmas are greatly simpliﬁed. For example, the following is the substitution lemma
for the CPS transformation.
[[M ]][Ψ(V )/x] = [[M [V /x]]]
where Ψ(V ) is deﬁned as follows: Ψ(x) = x and Ψ(λx.M ) =λx.[[M ]]. This is one of the key lemmas in Plotkin’s proof,
and its proof there requires 23 lines. The following is theproof of the lemma in Isabelle. It is proved by induction
on the structure of M, followed by the automatic theoremproving tactics auto.
lemma [[isValue V; closed V]] =⇒([M[V/x]]) = ([M])[Ψ(V)/(x~)]
by(induct M,auto)If we adopt the unparameterized abstract syntax, the proof
gets more complicated. The statement of the lemma must
explicitly mention that M does not contain 0, 1 and 2 asvariables.
The main part of our veriﬁcation is based on Plotkin’s
proof. Plotkin introduced the auxiliary transformation M :K,
called the colon transformation, and showed the correctnessof the CPS transformation by the following properties.
1. [[M ]]K →∗ M :K (if K is a closed value).

2. If M → N then M :K →∗ N :K (if K is a closed value).
Plotkin’s proofs of these properties require 17 and 25 lines,
respectively. Our proof scripts of these lemmas consist of 82
and 90 lines. It was not very diﬃcult to translate Plotkin’s
proofs into the proofs in Isabelle.

4. DANVY AND NIELSEN’S CPS TRANSFORMATION
4.1 Formalization of the transformation
We veriﬁed an optimized version of the CPS transformation by Danvy and Nielsen [5]. This veriﬁcation was much
more diﬃcult than our veriﬁcation of Plotkin’s CPS transformation. In addition to the problem we described in theprevious section, we encountered several other problems informalizing and proving the correctness of the transformation. We outline our formalization mostly without using thesyntax of Isabelle. The concrete formalization in Isabelle
can be obtained by translating the material in this section.
Danvy and Nielsen’s CPS transformation avoids introducing redundant β-redexes. For comparison, let us consider thefollowing Plotkin’s transformation:[[x1 x2 ]](λy.y) = (λk.(λk.kx1 )(λm.(λk.kx2 )(λn.mnk)))(λy.y)where many redundant redexes are introduced by the transformation. Danvy and Nielsen’s transformation is one of
the CPS transformations that avoid introducing these redundant redexes. Their transformation is deﬁned as thefollowing mutually recursive transformations:Ψ(x)Ψ(λx.M )==xλx.λk.[[M ]]k[[V ]]K[[V0 V1 ]]K[[V0 M1 ]]K[[M0 V1 ]]K[[M0 M1 ]]K

=
=
=
=
=

KΨ(V )
Ψ(V0 )Ψ(V1 )K[[M1 ]](λa1 .Ψ(V0 )a1 K)[[M0 ]](λa0 .a0 Ψ(V1 )K)[[M0 ]](λa0 .[[M1 ]](λa1 .a0 a1 K))

where Ψ(V ) and [[M ]] are transformations of values andterms, respectively. A continuation K is given as an argument of the transformation [[M ]]. For example, x1 x2 with
continuation λy.y is transformed into the following term:[[x1 x2 ]](λy.y) = x1 x2 (λy.y)where no redundant redex is introduced.
The ﬁrst problem with this transformation concerns fresh
variables introduced in the transformation. For Danvy andNielsen’s CPS transformation, it is not enough to introduce
a ﬁxed number of fresh variables. In the speciﬁcation, there
are three variables introduced by the transformation: k, a0
and a1 . However, many instances of the variable a0 are
required simultaneously. The following example clariﬁes the
problem.
[[x1 x2 (x3 x4 x5 )]](λy.y) =x1 x2 (λa0 .x3 x4 (λa0 .a0 x5 (λa1 .a0 a1 (λy.y))))During the computation of x3 x4 , the value of x1 x2 must
be preserved. Thus, a0 and a0 must be diﬀerent variables.
This is not clear from the deﬁnition and we ﬁrst thoughtthat it was enough to introduce the three variables a0 , a1
and k as in Plotkin’s CPS transformation. However, in thespeciﬁcation, it is assumed that clashes of variable names areresolved by renaming bound variables. Since this renaming
is not performed automatically, it is not possible to formalize
the speciﬁcation, above, directly in Isabelle.
To eliminate implicit renaming of the variable a0 , we takethe approach of generating fresh variables explicitly. Most
compilers obtain fresh variables in this approach. We revise
the deﬁnition of the transformation so that the transformation [[·]]i is indexed by a natural number, which is used togenerate fresh variables. The following is the deﬁnition of
the revised transformation:[[V ]]i K[[V0 V1 ]]i K[[V0 M1 ]]i K[[M0 V1 ]]i K[[M0 M1 ]]i K

=
=
=
=
=

KΨ(V )
Ψ(V0 )Ψ(V1 )K[[M1 ]]i (λai .Ψ(V0 )ai K)[[M0 ]]i (λai .ai Ψ(V1 )K)[[M0 ]]i (λai .[[M1 ]]i+1 (λai+1 .ai ai+1 K))

where we assume there are fresh variables ai indexed by anatural number i.
We ﬁrst formalized Danvy and Nielsen’s transformation
based on this speciﬁcation. As Plotkin’s CPS transformation, the source and target languages are formalized by thesame abstract syntax parameterized with the type of variables. We represented the variables after the translation
with the following datatype:
datatype ’a variable = Orig ’a| Avar nat| k("_~")("_~~")

where x~ and i~~ represent the variable x in the source language and ai introduced by the transformation, respectively.
Then the speciﬁcation can be formalized as functions withthe following types:
constsPsi:: ’a lt => ’a lt’
CPS:: [’a lt, nat, ’a lt’] => ’a lt’where ’a lt’ is an abbreviation of ’a variable lt.
The second problem concerns formalization of the transformation [[·]]i as a higher-order function: the transformationof a term is not a term, but a function from terms to terms.
The automated theorem-proving tactics of Isabelle do notwork eﬀectively for this speciﬁcation, so that even very simple lemmas cannot be proved automatically. Thus, it was
not feasible to do veriﬁcation based on this speciﬁcation.
To solve this problem, we reformulated the transformation
as a function from terms into contexts. To represent thetransformation we introduced context C deﬁned as follows:
C ::= [ ] | λai .C | M C | CM
The following is the reformulation of the transformation: wewrite ([M ])i for the transformation based on contexts.
([V ])i = [ ]Ψ(V )([V0 V1 ])i = Ψ(V0 )Ψ(V1 )[ ]([V0 M1 ])i = ([M1 ])i ◦ (λai .Ψ(V0 )ai [ ]))([M0 V1 ])i = ([M0 ])i ◦ (λai .ai Ψ(V1 )[ ])([M0 M1 ])i = ([M0 ])i ◦ (λai .[ ]) ◦ ([M1 ])i+1 ◦ (λai+1 .ai ai+1 [ ])where C1 ◦C2 is the composition of contexts C1 and C2 . This
reformulation is possible because K appears exactly once in[[M ]]K. We showed that two deﬁnitions are equivalent inIsabelle: [[M ]]i K = ([M ])i [K] where the operation C[N ] ﬁlls

the hole of C with N . Then we used the formalization basedon contexts in our veriﬁcation.
For the speciﬁcation based on contexts, it was possible toshow basic properties of the transformation with automatedtheorem-proving tactics. We ﬁrst extended basic operations
on terms such as the set of free variables and substitution
to contexts. Since the deﬁnitions of the most operations are
straightforward, we show only the deﬁnition of substitution
on contexts:[ ][N/x](λai .C)[N/x](M C)[N/x](M C)[N/x]

=
=
=
=

[]
λai .C[N/x]
M [N/x]C[N/x]
C[N/x]M [N/x]cannot be extended to a bijection is also sometimes useful.
The following relation is a renaming for the set of variables{xi | i ∈ N}.
{(xi , xi+1 ) | i ∈ N}
The extension of a renaming E ⊕ (x, y) is deﬁned as follows:E ⊕ (x, y) = {(a, b) | (a, b) ∈ E ∧ a = x ∧ b = y} ∪ {(x, y)}
We deﬁne a deductive system with judgments of the formE
M =α N , which means M and N are α-equivalent
under the renaming E. The deductive system is deﬁned asfollows:(x, y) ∈ E
E x =α ywhere the variable x is restricted to a variable of the source
language. Then the following properties of the transformation are veriﬁed with automated theorem-proving tactics.
• F V (M ) = F V (([M ])i )• ([M [V /x]])i = ([M ])i [Ψ(V )/x]
The third problem in veriﬁcation of the transformation
concerns the α-equivalence of terms. Danvy and Nielsen
proved the correctness of their CPS transformation by thefollowing property.
M →N⇒[[M ]]K →∗ [[N ]]K

However, this property does not hold in our formalization
based on abstract syntax with variable names. In fact,([M ])i [K] is not reduced to ([N ])i [K], but to a term that is
α-equivalent to ([N ])i [K]. Thus, we must show the following
property.
M →N⇒ ([M ])i [K] →∗ N  and([N ])i [K] =α N  for some N 

Veriﬁcation of this property requires formalization of αequivalence.

4.2 Formalization of α-equivalence
We found that the standard formalization of α-equivalence
was not natural for our formalization and cumbersome for
automated theorem proving.
The operational semantics itself can be formalized without
considering α-conversion and thus the set of variables canbe ﬁnite. However, if the set of variables is ﬁnite, then thestandard formalization of α-equivalence is not suﬃcient toderive the equivalence of terms. For example, if we have
only two variables x and y, the following equivalence cannot
be derived.
λx.λy.xy =α λy.λx.yx
Furthermore, it is rather diﬃcult to derive α-equivalenceof terms automatically in the standard formalization, because the standard formalization of α-equivalence contains
the rule of transitivity and is not syntax-directed. Thus, it
is not straightforward to determine whether two terms are
α-equivalent automatically.
To overcome these issues, we formalized α-equivalence asa syntax-directed deductive system. Let Var be the set ofvariables. We say E ⊆ Var × Var is a renaming if (x, y) ∈ E
and (x , y  ) ∈ E implies x = x ⇔ y = y  . Any renaming
can be extended to a permutation on the set of variables
if the set of variables is ﬁnite. However, a renaming thatEE ⊕ (x, y)M =α M 

λx.M =α λy.M E

M =α M  E N =α N 
E M N =α M  N 

We write
M =α N if ID
M =α N where ID is theidentity relation on the set of variables.

4.3

Alpha-equivalence in verification

Based on the deductive system of α-equivalence we veriﬁed Danvy and Nielsen’s CPS transformation. In our veriﬁcation, it was necessary to show the following α-equivalence:([M ])i [K] =α ([M ])i+1 [K]where F V (K) ∩ {ai | i ∈ N} = ∅. Please note the set ofvariables in the target language of the transformation is theunion of the set of variables of the source language Varsrc
and the set of variables introduced by the transformation{ai | i ∈ N} ∪ {k}.
In order to prove the property above, we ﬁrst extended
α-equivalence to contexts as follows:E[ ] =α [ ]EC =α C (ai , aj ) ∈ E
E λai .C =α λaj .C

E

M =α M  E C =α C
E M C =α M  CE

M =α M  E C =α C
E CM =α C M This deductive system is designed so that the following property holds.
• If E C =α C and E
C [M  ].

M =α M  then E

C[M ] =αThen we proved the α-equivalence above in the following
manner.
1. It is suﬃcient to show the following property:ID ∪ {(ai , ai+1 ) | i ∈ N}([M ])i [K] =α ([M ])i+1 [K]

where ID is {(x, x) | x ∈ Varsrc } ∪ {(k, k)}. It is because F V (([M ])i [K]) ∩ {ai | i ∈ N} = ∅.
2. We decompose the relation into the following relations
with the property of α-equivalence on contexts.
ID ∪ {(ai , ai+1 ) | i ∈ N}([M ])i =α ([M ])i+1

ID ∪ {(ai , ai+1 ) | i ∈ N}

K =α Kx ∈ BVU

M ∈ BVU
λx.M ∈ BVU
M ∈ BVUN ∈ BVU

M ∈ BVUN ∈ BVU F V (M N ) ∩ LBV(M N ) = ∅M N ∈ BVU

F V (let x = M in N ) ∩ LBV(let x = M in N ) = ∅let x = M in N ∈ BVU

Figure 3: Bound variable uniqueness3. The ﬁrst relation is proved by induction on structureof M . The second relation is obtained from F V (K) ∩{ai | i ∈ N} = ∅.
There is another important property of α-equivalence toshow correctness of Danvy and Nielsen’s transformation: αequivalence and reduction commute.
• If L =α M and M → N then L → N  and N  =α N
for some N  .
This does not hold for the λ-calculus formalized with variable names where reduction of open terms is considered [18].
In our formalization, α-equivalence and reduction commute
because V in the reduction (λx.M )V → M [V /x] is restricted
to a closed term. The property is proved from the following
substitution lemma on α-equivalence.
• If E ⊕ (x, y)M =α M  and ∅E M [V /x] =α M  [V  /y].

preserved by reduction. We write LBV(M ) for the set of
let-bound variables of M deﬁned as follows:
LBV(V ) = ∅LBV(M0 M1 ) = LBV(M0 ) ∪ LBV(M1 )LBV(let x = M0 in M1 ) = {x} ∪ LBV(M0 ) ∪ LBV(M1 )Note that let-bound variables inside lambda abstractions are
not included in LBV(V ). Based on this deﬁnition, we inductively deﬁned the set of terms BVU where let-bound variables are uniquely used. The deﬁnition is shown in Figure 3.
The following property of BVU ensures that no name clash
occurs when a term in BVU is transformed.
• If M ∈ BVU then LBV(M ) ∩ F V (M ) = ∅.
It is also shown that BVU is closed under substitution.

V =α V  then

• If M, V ∈ BVU and V is a closed value then M [V /x] ∈BVU.

4.4 Verification for let-expressions
We extend our veriﬁcation of Danvy and Nielsen’s transformation to the language with let-expressions. This veriﬁcation illustrates that it is essential to impose uniqueness ofbound variables in a source term in order to simplify veriﬁcation of some program transformations. We consider thefollowing extended language.
M ::= x | λx.M | M M | let x = M in M

This holds because the let-bound variables inside lambda
abstraction are not included in LBV(V ). From this property,
it is shown that BVU is preserved by reduction: if M ∈ BVU
and M → N then N ∈ BVU.
For veriﬁcation of the transformation we showed that thefollowing two key lemmas by assuming that M is in BVU.
The proofs cannot be automated as much as those for the
language without let-expressions.

Danvy and Nielsen’s transformation on let-expressions is deﬁned as follows:• If M ∈ BVU then F V (M ) = F V (([M ])i ).

[[let x = V0 in M1 ]]K[[let x = M0 in M1 ]]K• If M ∈ BVU then ([M [V /x]])i = ([M ])i [Ψ(V )/x].

==

let x = Ψ(V0 ) in [[M1 ]]K[[M0 ]](λa0 .let x = a0 in [[M1 ]]K)

For this transformation, a clash of variable names may happen if a variable name is not uniquely used in a source term.
In the following example, the free variable x in the the source
term is made bound by the transformation.

With these lemmas, the rest of the veriﬁcation was almost
the same as that of Danvy and Nielsen’s transformation
without let-expressions.

[[(let x = y in x)x]](λz.z) = let x = y in x(λa0 .a0 x(λz.z))
Danvy and Filinski solved this clash of variable names byintroducing an explicit renaming into their version of the
CPS transformation [4]. We ﬁrst tried their approach, but
introducing renaming into the transformation makes it very
diﬃcult to prove properties of the transformation.
This kind of variable name clashes are usually solved byassuming that all bound variables are distinct in compilers.
This assumption makes implementation of the transformation much simpler. We basically took this approach, but
adopted a weaker assumption on variable names because
the property that all bound variables are distinct is not

5.

DANVY AND FILINSKI’S CPS TRANSFORMATIONWe also veriﬁed Danvy and Filinski’s CPS transformation. Danvy and Filinski’s transformation is deﬁned withthe two-level lambda and more complicated than Danvy
and Nielsen’s transformation. However, we could verify thetransformation with the same techniques used for Danvy andNielsen’s transformation. Danvy and Nielsen’s transformation was derived from Danvy and Filinski’s CPS transformation by unfolding and folding [5].
The transformation is formalized with the two-level lambda

([...])i([x])i([λx.M ])i([M1 M2 ])i

:
=
=
=

syntax → context × syntax([ ], x)([ ], λx.λk.([M ]) [k])(fst(([M1 ])i ) ◦ fst(([M2 ])i+1 ) ◦ snd(([M1 ])i )snd(([M2 ])i+1 )(λai .[ ]), ai )([...])
([x])
([λx.M ])
([M1 M2 ])

:
=
=
=

syntax → context[ ]x[ ](λx.λk.([M ]) [k])fst(([M1 ])0 ) ◦ fst(([M2 ])1 ) ◦ snd(([M1 ])0 )snd(([M2 ])1 )[ ]Figure 4: Reformulation of Danvy and Filinski’s CPS transformation with contexts
calculus as follows:[[...]][[x]][[λx.M ]][[M1 M2 ]]

:
=
=
=

syntax → (syntax → syntax) → syntax
λκ.@κxλκ.@κ(λx.λk.@[[M ]] k)λκ.@[[M1 ]](λm.@[[M2 ]](λn.mn(λa.@κa)))[[...]]
[[x]]
[[λx.M ]]
[[M1 M2 ]]

:
=
=
=

syntax → syntax → syntax
λk.kx
λk.k(λx.λk.@[[M ]] k)
λk.@[[M1 ]](λm.@[[M2 ]](λn.mnk))

The overlined λ and @ correspond to functional abstractions
and applications in the translation program and they are
reduced at translation time. Thus, only the other abstractions and applications remain after translation. The transformation is formalized as two mutually recursive transformations to preserve tail-calls. A whole program is translated
as @[[M ]](λm.m).
We encountered the basically same diﬃculties in formalizing and verifying this transformation as those in Danvy
and Nielsen’s transformation. To avoid clashes of variablenames, we formalized the transformation as follows:[[x]]i = λκ.@κx[[λx.M ]]i = λκ.@κ(λx.λk.@[[M ]] k)[[M1 M2 ]]i = λκ.@[[M1 ]]i (λm.@[[M2 ]]i+1 (λn.mn(λai .@κai )))[[x]] = λk.kx[[λx.M ]] = λk.k(λx.λk.@[[M ]] k)[[M1 M2 ]] = λk.@[[M1 ]]0 (λm.@[[M2 ]]1 (λn.mnk))
where we assume there are fresh variables ai indexed by anatural number i.
Further, we reformulated the transformation with contexts for veriﬁcation. We could do that because [[M ]]i canalways be written λk.C[kV ] for some C and V . The reformulation of the transformation with contexts is shown in
Figure 4. This speciﬁcation of the transformation is not
intuitive, but it was still easier to reason about it with automated theorem-proving tactics than the higher-order speciﬁcation above.
With this formalization of the transformation, veriﬁcation of its correctness was analogous to that of Danvy andNielsen’s transformation.

6. RELATED WORK
We have chosen ﬁrst-order abstract syntax with variablenames as representation of terms. McKinna and Pollack
also formalized a theory of pure type systems in the theorem

prover LEGO, with abstract syntax with variable names [10].
Recently, the Church-Rosser property of the lambda calculus was shown in Isabelle/HOL based on abstract syntax
with variable names [18]. Formalization of reduction in theseworks diﬀers from that of our work in the sense that theymust consider β-reduction of open terms.
Another approach to abstract syntax uses de Bruijn indexes to represent bound variables. This approach has theadvantage that α-equivalent terms have unique representation. This approach was taken by several works formalizing
theory of programming languages in Isabelle/HOL [11, 1].
However, we think that the de Bruijn notation makes it diﬃcult to formalize and reason about program transformations,as we discussed in Section 2. For example, formalization of
Danvy and Filinski’s CPS transformation based on de Bruijn
indexes would be very complicated.
The third approach uses higher-order abstract syntax [15],where object-level abstractions are represented by metalevel abstractions. This approach often simpliﬁes the formalization of binding in theorem provers, and is used for
veriﬁcation in theorem provers based on a logical framework [8]. However, it was reported that higher-order abstract syntax is diﬃcult to treat in theorem provers such as
Isabelle/HOL and Coq [7].
Danvy, Dzaﬁc and Pfenning showed some syntactic properties of Danvy and Filinski’s transformation [3]. They formalized their proofs in Elf, a constraint logic-programming
language based on the logical framework [9, 14]. Their formalization is based on higher-order abstract syntax and thus
they do not have the problems of fresh variables and αequivalence. Instead, they needed to reformulate the transformation as a deductive system.

7.

CONCLUSIONS

We have veriﬁed several versions of the CPS transformations based on abstract syntax with variable names. The
main obstacles in our veriﬁcation was treatment of variablenames. First, we have shown that freshness of variables introduced by a transformation can be imposed by abstract
syntax parameterized with the type of variables. Secondly,
formalization of α-equivalence as a deductive system makes
it possible to show α-equivalence by automated theoremproving tactics. Finally, uniqueness of let-bound variables is
imposed to simplify Danvy and Nielsen’s transformation extended for let-expressions. Even though we needed to devise
these methods, we think that it is feasible to verify correctness of program transformations based on abstract syntax
with variable names.

Acknowledgments
This work is partially supported by Japan Society for the
Promotion of Science, Grant-in-Aid for Encouragement ofYoung Scientists of Japan, No. 13780193, 2001.

8. REFERENCES[1] S. Ambler and R. L. Crole. Mechanized operationalsemantics via (co)induction. In Proceedings of 12th
International Conference on Theorem Proving in
Higher Order Logics, volume 1690 of LNCS, pages
221–238, 1999.
[2] A. W. Appel. Compiling with Continuation.
Cambridge University Press, 1992.
[3] O. Danvy, B. Dzaﬁc, and F. Pfenning. On proving
syntactic properties of CPS programs. In Proceedingsof International Workshop on Higher Order
Operational Techniques in Semantics, volume 26 of
ENTCS, 1999.
[4] O. Danvy and A. Filinski. Representing control: astudy of the CPS transformation. Mathematical
Structures in Computer Science, 2(4):361 – 391, 1992.
[5] O. Danvy and L. R. Nielsen. A ﬁrst-order one-pass
CPS transformation. In Proceedings of Foundations ofSoftware Science and Computation Structures,
FOSSACS, volume 2303 of LNCS, pages 98–113, 2002.
[6] N. de Bruijn. Lambda calculus notation with namelessdummies, a tool for automatic formula manipulation,with application to the Church-Rosser theorem.
Indagationes Mathematicae, 34:381–391, 1972.
[7] J. Despeyroux and A. Hirschowitz. Higher-ordersyntax and induction in Coq. In F. Pfenning, editor,
Proceedings of the Fifth International Conference on
Logic Programming and Automated Reasoning(LPAR), volume 822 of LNAI, pages 159–173, 1994.
[8] J. Hannan and F. Pfenning. Compiler veriﬁcation in
LF. In Proceedings of the Seventh Annual IEEE
Symposium on Logic in Computer Science, pages
407–418, 1992.
[9] R. Harper, F. Honsell, and G. Plotkin. A frameworkfor deﬁning logics. Journal of the ACM,
40(1):143–184, 1993.
[10] J. McKinna and R. Pollack. Some lambda calculus
and type theory formalized. Journal of AutomatedReasoning, 23:373–409, 1999.
[11] T. Nipkow. More Church-Rosser proofs (inIsabelle/HOL). Journal of Automated Reasoning,
26:51–66, 2001.
[12] T. Nipkow, L. C. Paulson, and M. Wenzel.
Isabelle/HOL: A Proof Assistant for Higher-Order
Logic, volume 2283 of LNCS. Springer-Verlag, 2002.
[13] L. C. Paulson. Isabelle: A Generic Theorem Prover,volume 828 of LNCS. Springer, 1994.
[14] F. Pfenning. Logic programming in the LF logicalframework. In G. Huet and G. Plotkin, editors, Logical
Frameworks, pages 149–181. Cambridge University
Press, 1991.
[15] F. Pfenning and C. Elliott. Higher-order abstract
syntax. In Proceedings of the ACM SIGPLAN ’88
Symposium on Language Design and Implementation,
pages 199–208, 1988.
[16] G. D. Plotkin. Call-by-name, call-by-value and the

λ-calculus. Theoretical Computer Science,
1(2):125–159, December 1975.
[17] G. L. Steele Jr. Rabbit: A compiler for Scheme.
Master’s thesis, MIT, 1978.
[18] R. Vestergaard and J. Brotherston. A formalisedﬁrst-order conﬂuence proof for the λ-calculus using
one-sorted variable names (Barendregt was right after
all ... almost). In Proceedings of the 12th International
Conference Rewriting Techniques and Applications,volume 2051 of LNCS, pages 306–321, 2001.
[19] M. Wenzel. Isar — a generic interpretative approachto readable formal proof documents. In Proceedings ofthe 12th International Conference on Theorem
Proving in Higher Order Logics, volume 1690 of
LNCS, pages 167–183, 1999.