Runtime Behavior of Conversion Interpretationof Subtyping
Yasuhiko Minamide
Institute of Information Sciences and Electronics
University of Tsukuba
and
PRESTO, JSTminamide@is.tsukuba.ac.jp

Abstract. A programming language with subtyping can be translated
into a language without subtyping by inserting conversion functions. Previous studies of this interpretation showed only the extensional correctness of the translation. We study runtime behavior of translated programs and show that this translation preserves execution time and stackspace within a factor determined by the types in a program. Both theproofs on execution time and stack space are based on the method of logical relations where relations are extended with the factor of slowdown
or increase of stack space.

1

Introduction

A programming language with subtyping can be translated into a language without subtyping by inserting conversion functions. Previous studies of this interpretation showed only the extensional correctness of the translation [3, 13]. In thispaper, we study runtime behavior of the conversion interpretation of subtyping
in call-by-value evaluation. We show that this translation preserves execution
time and stack space within a factor determined by the types in a program, if
subtyping relation is a partial order.
The translation of conversion interpretation changes the runtime behavior ofprograms in several respects. It inserts conversion functions and may increase
the total number of closures allocated during execution. It translates tail-calls
into non-tail-calls and, therefore, it may increase stack space usage. Although
the translation causes these changes of runtime behavior, execution time andstack space usage are preserved asymptotically. This contrasts with type-directed
unboxing of Leroy where both time and space complexity are not preserved [11].
Type systems with subtyping can be used to express information obtained byvarious program analyses such as control ﬂow analyses [7]. One strategy of utilizing types obtained by program analysis is to adopt conversion interpretation of
the subtyping. For example, it is possible to choose an optimized representationof values based on types and to insert conversion functions as type-directed unboxing of polymorphic languages [8]. In order to adopt this compilation method

we need to show that the conversion interpretation is safe with respect to performance. The results in this paper ensure safety with respect to execution timeand stack space.
Both the safety proofs on execution time and stack space are based on themethod of logical relations. The method of logical relations has been used forcorrectness proofs of many type-directed program transformations [8, 14, 12] andwas extended to prove time safety of unboxing by Minamide and Garrigue [11].
One motivation of this work is to show that the method of logical relations can beextended to prove safety with respect to stack space. The structure of the proof
we obtained for stack space is almost the same as that for the execution time.
This is because the operational semantics proﬁling stack space can be formalized
in the same manner as the semantics proﬁling execution time. We believe this is
the ﬁrst proof concerning stack space based on the method of logical relations.
We believe that the conversion interpretation is also safe with respect toheap space. However, it seems that it is diﬃcult to extend the method of logicalrelations for heap space. We would like to study safety with respect to heap
space in future work.
This paper is organized as follows. We start with a review of conversion interpretation and runtime behavior of translated programs. In Section 3 we deﬁne
the language we will use in the rest of the paper and formally introduce conversion interpretation. We prove that conversion interpretation preserves stackspace and execution time in Section 4 and Section 5. Finally we review related
work and presents the conclusions.

2

Review of Conversion Interpretation

We review conversion interpretation of subtyping and intuitively explain that theinterpretation preserves stack space and execution time if the subtyping relation
is a partial order. Since the subtyping relation is transitive and reﬂexive, thesubtyping relation is a partial order if it contains no equivalent types.
The conversion interpretation is a translation from a language with subtyping
into a simply typed language without subtyping. The idea is to insert a conversion function (or coercion) where the subsumption rule is used. If the following
subsumption rule is used in the typing derivation,Γ M :τ τ ≤σΓ M :σthe conversion function coerceτ≤σ of type τ → σ is inserted and we obtain thefollowing term.
coerce τ≤σ (M )Coercion coerce τ≤σ is inductively deﬁned on structure of types. If there are twobase types bigint and int for integers where int is a subtype of bigint, we need tohave a coercion primitive int2bigint of type int → bigint. A conversion function
on function types is constructed as follows.
λf.λx.coerceτ2 ≤σ2 (f(coerce σ1 ≤τ1 (x)))
This is a coercion from τ1 → τ2 to σ1 → σ2 .
We show that this interpretation of subtyping is safe with respect to execution
time and stack space if the subtyping relation is a partial order. Intuitively, thisholds because only a ﬁnite number of coercions can be applied to any value. If
a subtyping relation is not a partial order, i.e., there exist two types τ and σsuch that τ ≤ σ and σ ≤ τ , we can easily construct counter examples for both
execution time and stack space. A counter example for execution time is thefollowing translation of term M of type τ ,coerce σ≤τ (coerce τ≤σ (. . . (coerce σ≤τ (coerce τ≤σ (M )))))
where τ ≤ σ and σ ≤ τ . The execution time to evaluate the coercions in thetranslation depends on the number of the coercions and cannot be bounded by aconstant. It may be possible to avoid this silly translation, but it will be diﬃcult
to avoid this problem in general if we have equivalent types.
The conversion interpretation translates tail-call applications into non-tailcall applications. Let us consider the following translation of application x y.
coerce τ≤σ (x y)Even if x y is originally at a tail-call position, after translation it is not at a
tail-call position. Therefore, it is not straightforward to show the conversion
interpretation preserves stack space asymptotically. In fact, if we have equivalent
types, we can demonstrate a counter example. Let us consider the following
program where types A and B are equivalent.
fun f (0, x : A) = x| f (n, x : A) = g (n-1, x)
and g (n, x : A) = f (n, x) : B(* f: int * A -> A *)(* g: int * A -> B *)We have a type annotation f (n, x) : B in the body of g and thus g has typeA -> B. This program contains only tail-calls, and thus requires only constant
stack space. By inserting conversion functions we obtain the following program:fun f (0, x : A) = x| f (n, x : A) = B2A (g (n-1, x))
and g (n, x : A) = A2B (f (n, x))
where A2B and B2A are coercions between A and B. For this program, evaluationof f n requires stack space proportional to n since both the applications of f
and g are not tail-calls.
In order to preserve time and stack space complexity, it is essential thatthe subtyping relation is a partial order. This ensures that there is no inﬁnite
subtyping chain of types if we consider only structural subtyping. Thus only aﬁnite number of conversions can be applied to any value if the subtyping relation
is a partial order.

3

Language and Conversion Interpretation

In this section we introduce a call-by-value functional language with subtyping
and its conversion interpretation. We consider a call-by-value functional languagewith the following syntax.
V ::= x | i | i | λx.M | fixn x.λy.M
M ::= V | M M | let x = M in M
There are two families of integers: i and i are integer values of types bigint
and int respectively. The language includes bounded recursive functions where
fixn x.λy.M is expanded at most n times [4]. Any closed program with usual
recursive functions can be simulated by bounded recursive functions.
For this language we consider a simple type system extended with subtyping.
The types of the language are deﬁned as follows.
τ ::= bigint | int | τ → τ
We consider two base types bigint and int where int is a subtype of bigint. A
metavariable σ is also used to denote a type. The subtyping relation τ1 ≤ τ2 isgiven by the following three rules.
τ ≤τ

int ≤ bigint

σ1 ≤ τ1 τ2 ≤ σ2
τ1 → τ2 ≤ σ1 → σ2

The rule for transitivity is not included here because it can be derived from theother rules for this subtyping relation. We write τ < σ if τ ≤ σ and τ ≡ σ. It
is clear that the subtyping relation is a partial order. The typing judgment has
the following form:Γ  M :τwhere Γ is a type assignment of the form x1 :τ1 , . . . , xn :τn . The rules of the typesystem are deﬁned as follows.
Γ  i:bigint

Γ  i:int

x:τ ∈ ΓΓ  x:τΓ  M1 :τ1 → τ2 Γ  M2 :τ1
Γ  M1 M2 :τ2

Γ, x:τ1  M :τ2
Γ  λx.M :τ1 → τ2

Γ  M :σ σ ≤ τΓ  M :τΓ, y:τ1 → τ2 , x:τ1  M :τ2
Γ  fixn y.λx.M :τ1 → τ2

Γ  M1 :τ1 Γ, x:τ1  M2 :τΓ  let x = M1 in M2 :τ

Note that let-expressions do not introduce polymorphic types. They are used
to simplify deﬁnition of coercions.

We consider a standard natural semantics for this language. A judgment has
the following form: M ⇓ V . The rules are given as follows.
M1 ⇓ V1 M2 [V1 /x] ⇓ V
let x = M1 in M2 ⇓ V

V ⇓V
M1 ⇓ λx.M

M1 ⇓ fixk+1 y.λx.M

M2 ⇓ V2 M [V2 /x] ⇓ V
M1 M2 ⇓ V

M2 ⇓ V2 M [fixk y.λx.M/y][V2 /x] ⇓ V
M1 M2 ⇓ V

When the recursive function fixk+1 y.λx.M is applied, the bound of the recursivefunction is decremented.
To formalize the conversion interpretation we need to introduce a target
language without subtyping that includes a coercion primitive. We consider thefollowing target language. The only extension is the coercion primitive int2bigint
from int into bigint.
W ::= x | i | i | λx.N | fixn x.λy.N
N ::= W | N N | let x = N in N | int2bigint(N )The operational semantics and type system of the language are almost the sameas those of the source language. The rule of subsumption is excluded from thetype system. The typing rule and evaluation of coercion are deﬁned as follows.
N ⇓iint2bigint(N ) ⇓ iΓ  N :int
Γ  int2bigint(N ):bigint

The conversion interpretation is deﬁned inductively on structure of the typing
derivation of a program: the translation C[[Γ  M :τ ]] below gives a term of thetarget language.
C[[Γ  x:τ ]] = x
C[[Γ  λx.M :τ1 → τ2 ]] = λx.C[[Γ, x:τ1  M :τ2 ]]C[[Γ  fixn y.λx.M :τ1 → τ2 ]] = fixn y.λx.C[[Γ, y:τ1 → τ2 , x:τ1  M :τ2 ]]C[[Γ  M1 M2 :τ2 ]] = C[[Γ  M1 :τ1 → τ2 ]]C[[Γ  M2 :τ1 ]]C[[Γ  M :τ ]] = coerce σ≤τ (C[[Γ  M :σ]])C[[Γ  let x = M1 in M2 :τ2 ]] = let x = C[[Γ  M1 :τ1 ]] in C[[Γ  M2 :τ2 ]]The coercion used in the translation is deﬁned inductively on structure of derivation of subtyping as follows 1 .
coerce τ≤τ (M ) = M
coerce int≤bigint (M ) = int2bigint(M )coerce τ1 →τ2 ≤σ1 →σ2 (M ) = let x = M in λy.coerce τ2 ≤σ2 (x(coerce σ1 ≤τ1 (y)))
Note that coerce τ≤τ (M ) must be not only extensionally equivalent to M , butalso intensionally equivalent to M . If we adopt (λx.x) M for coerce τ≤τ (M ), we
have the same problem when we have equivalent types, and thus execution timeand stack space are not preserved.
We deﬁne two measures, τ and τ , of types as follows.
int = 0bigint = 1
τ1 → τ2 = τ1 + τ2

int = 1bigint = 0
τ1 → τ2 = τ1 + τ2

It is clear that σ < τ implies σ < τ and σ > τ . Since τ and τ are
non-negative integers, we also obtain the following properties.
τn < . . . < τ1 < τ0⇒

τn < . . . < τ1 < τ0⇒n ≤ τ0τ0 < τ1 < . . . < τn⇒

τ0 > τ1 > . . . > τn⇒n ≤ τ0From the property we can estimate the maximum number of conversions applieda value of τ0 . In the following program, we know that n ≤ τ0 by the property.
coerce τn−1 ≤τn (. . . (coerce τ0 ≤τ1 (V ))Intuitively, this is the property that ensures that conversion interpretation preserves execution time and stack within a factor determined by types in a program.

4

Preservation of Stack SpaceWe show that coercion interpretation of subtyping preserves stack space within afactor determined by types occurring in a program. Strictly speaking, the factor
is determined by the types occurring in the typing derivation used in translationof a program. We prove this property by the method of logical relations.
First we extend the operational semantics to proﬁle stack space usage. The
extended judgment has the form M ⇓n V where n models the size of stack spacerequired to evaluate M to V . The following are the extended rules.
1

V ⇓ V
1

M1 ⇓m V1 M2 [V1 /x] ⇓n V
let x = M1 in M2 ⇓max(m+1,n) V

We assume that τ1 → τ2 ≤ τ1 → τ2 is not derived from τ1 ≤ τ1 and τ2 ≤ τ2 , butfrom the axiom.

M1 ⇓l λx.M M2 ⇓m V2 M [V2 /x] ⇓n V
M1 M2 ⇓max(l+1,m+1,n) V
M1 ⇓l fixk+1 y.λx.M M2 ⇓m V2 M [fixk y.λx.M/y][V2 /x] ⇓n V
M1 M2 ⇓max(l+1,m+1,n) V
This semantics is considered to model evaluation by an interpreter: M ⇓n V
means that a standard interpreter requires n stack frames to evaluate M to V .
In the rule of application, evaluation of M1 and M2 are considered as non-tailcalls and evaluation of the body of the function is considered as a tail-call. Thisis the reason that the number of stack frames used to evaluate the application
is max(l + 1, m + 1, n).
This semantics and the correspondence to a semantics modeling evaluation
after compilation is discussed in [10]: the ratio to the stack space used by compiled executable code is bounded by the size of a program.
By the rule for values, a value V is evaluated to itself with 1 stack frame.
Instead, you can choose V ⇓0 V as the rule for values. This choice does notmatter much because the diﬀerence caused by the choice is always only 1 stack
frame. We have chosen our rule to simplify our proofs.
We write e ⇓n if e ⇓n v for some v and e ⇓≤n if e ⇓m for some m ≤ n.
The main result of this section is that the conversion interpretation preserves
stack space within a factor determined by the sizes of types appearing in a
program.
Theorem 1. Let C[[∅  M :τ ]] = N and let C be an integer such that C > σ +3
for all σ appearing in the derivation of ∅  M :τ . If M ⇓n V then N ⇓≤Cn W
for some W .
Let us consider the following translation where the type of λx.1 is obtainedby subsumption for int → int ≤ int → bigint.
C[[(λx.1)2]] = (let y = λx.1 in λz.int2bigint(y z))2
The source program is evaluated with 2 stack frames.
(λx.1)2 ⇓2 1
On the other hand, the translation is evaluated with 4 stack frames.
(λx.1) 2 ⇓2 1
V ⇓ V 2 ⇓ 2 int2bigint((λx.1) 2) ⇓3 1
(λz.int2bigint((λx.1) z)) 2 ⇓3 1
λx.1 ⇓1 λx.1
(let y = λx.1 in λz.int2bigint(y z))2 ⇓3 1
1

1

where V ≡ λz.int2bigint((λx.1) z). In this case, the factor of increase is 3/2.
We prove the main theorem by the method of logical relations. Before deﬁning
the logical relations we deﬁne the auxiliary relation V1 V2 ↓n V deﬁned as follows.
M [V2 /x] ⇓n V
(λx.M )V2 ↓n V

M [V2 /x][fixk y.λx.M/y] ⇓n V
(fixk+1 y.λx.M )V2 ↓n V

By using this relation we can combine the two rules for the evaluation of theapplication into the following rule.
M1 ⇓l V1 M2 ⇓m V2 V1 V2 ↓n V
M1 M2 ⇓max(l+1,m+1,n) V
This reformulation simpliﬁes the deﬁnition of the logical relations and our proof.
We deﬁne logical relations V ≈C
τ W indexed by a type τ and a positive integer
C as follows.
i ≈C
int i
V ≈C
bigint i
V ≈C
τ1 →τ2 W

V = i or V = in+1
V2
for all V1 ≈Cτ1 W1 , if V V1 ↓≤Cn+τ2 +3then W W1 ↓W2 and V2 ≈C
τ2 W2

We implicitly assume that V and W have type τ for V ≈Cτ W . The parameter C
corresponds to the factor of increase of stack space usage. Note that the increaseof stack space usage depends on only the range type τ2 of a function type τ1 → τ2 .
This is explained by checking the following translation of a function f of type
τ1 → τ2 2 .
coerce τ1 →τ2 ≤σ1 →σ2 (f) ≡ λy.coerce τ2 ≤σ2 (f coerce σ1 ≤τ1 (y))
In this translation, only the coercion coerce τ2 ≤σ2 causes increase of stack space
usage.
We ﬁrst show that a conversion from τ to σ behaves well with respect to thelogical relations.
2C
Lemma 1. If τ < σ and V ≈C
τ W then coerce τ≤σ (W ) ⇓ W and V ≈σ W forsome W .

Proof. By induction on derivation of τ < σ.
Case: int ≤ bigint. By the deﬁnition of V ≈C
int W , both V and W must be i forsome i. Since coerce int≤bigint (i) = int2bigint(i), we have int2bigint(i) ⇓2 i andi ≈Cbigint i.
Case: τ ≡ τ1 → τ2 and σ ≡ σ1 → σ2 where σ1 ≤ τ1 and τ2 ≤ σ2 . There are two
subcases: τ2 < σ2 and τ2 ≡ σ2 . We show the former case here. The proof thelatter case is similar.
coerce τ≤σ (W ) ⇓2 λy.coerce τ2 ≤σ2 (W (coerce σ1 ≤τ1 (y)))
m+1V2 . By induction hypothesis,
Let V0 ≈C
σ1 W0 and V V0 ↓coerce σ1 ≤τ1 (W0 ) ⇓≤2 W1and V0 ≈C
τ1 W1 for some W1 . By deﬁnition of the logical relations
W W1 ↓≤Cm+τ2 +3 W32

Strictly speaking, it is let x = f in λy.coerceτ2 ≤σ2 (x coerceσ1 ≤τ1 (y)).

and V2 ≈C
τ2 W3 for some W3 . Then we obtain the following evaluation.
W ⇓1 W coerce σ1 ≤τ1 (W0 ) ⇓≤2 W1 W W1 ↓≤Cm+τ2 +3 W3W (coerce σ1 ≤τ1 (W0 )) ⇓≤max(2,3,Cm+τ2 +3) W3
where max(2, 3, Cm + τ2 + 3) = Cm + τ2 + 3.
By induction hypothesis,
coerce τ2 ≤σ2 (W3 ) ⇓2 W2
and V2 ≈C
σ2 W2 for some W2 . Then
coerce τ2 ≤σ2 (W (coerce σ1 ≤τ1 (W0 ))) ⇓≤Cm+τ2 +4 W2
where Cm + τ2 + 4 ≤ Cm + σ2 + 3

The next lemma indicates that we can choose a constant C such that theevaluation of a source program and its translation are related by C. For ρ and ρ
two environments with the same domain, ρ ≈CΓ ρ means that they are pointwise
related. The main theorem is obtained by restricting this lemma to Γ = ∅ andtaking C such that C > σ + 3 for all σ appearing in the typing derivation.
Lemma 2. Let C be an integer such that C > σ for all σ appearing in thederivation of Γ  M :τ . Let C[[Γ  M :τ ]] = N and ρ ≈CΓ ρ.
If ρ(M ) ⇓n+1 V then ρ (N ) ⇓≤Cn+τ+3 W and V ≈CW
for some W .
τProof. By lexicographic induction on derivation of Γ  M :τ and the sum ofbounds of recursive functions in M .
Case: Γ  M :σ is derived from Γ  M :τ and τ ≤ σ. We assume τ < σ. The
case of τ ≡ σ is trivial. By deﬁnition, N must be coerceτ≤σ (N0 ) for someN0 and C[[Γ  M : τ ]] = N0 . By induction hypothesis,ρ (N0 ) ⇓≤Cn+τ+3 W0
and V ≈C
τ W0 for some W0 . By Lemma 1,
ρ (coerce τ≤σ (N0 )) ⇓≤Cn+τ+3+1 W
and V ≈C
σ W for some W . The proof of this case completes since Cn + τ +3 + 1 ≤ Cn + σ + 3.
Case: Γ  M1 M2 :τ2 is derived from Γ  M1 :τ1 → τ2 and Γ  M2 :τ1 . By thedeﬁnition of the translation N ≡ N1 N2 for some N1 and N2 .
ρ(M1 M2 ) ⇓k+1 V is derived from ρ(M1 ) ⇓l V1 and ρ(M2 ) ⇓m V2 and V1 V2 ↓n
V where l ≤ k, m ≤ k and n ≤ k + 1. By induction hypothesis for M1 ,ρ (N1 ) ⇓C(l−1)+τ1 →τ2 +3 W1


≤Cl+2
and V1 ≈C
W1 because
τ1 →τ2 W1 for some W1 . Then we have ρ (N1 ) ⇓τ1 → τ2 + 1 ≤ C. By induction hypothesis for M2 ,ρ (N2 ) ⇓C(m−1)+τ1 +3 W2
≤Cm+2
and V2 ≈C
W2 because
τ1 W2 for some W2 . Then we also have ρ (N2 ) ⇓τ1 + 1 ≤ C. By deﬁnition of the logical relations

W1 W2 ↓≤C(n−1)+τ2 +3 W
and V ≈C
τ2 W for some W . We have the following inequality.
max(Cl + 2 + 1, Cm + 2 + 1, C(n − 1) + τ2 + 3) ≤ Ck + τ2 + 3
Hence,
ρ (N1 N2 ) ⇓≤Ck+τ2 +3 W
Case: Γ  fixa+1 y.λx.M :τ1 → τ2 is derived from Γ, y:τ1 → τ2 , x:τ1  M :τ2 .
By deﬁnition, C[[Γ, y:τ1 → τ2 , x:τ1  M :τ1 ]] = N for some N .
We have the following evaluation.
ρ(fixa+1 y.λx.M ) ⇓1 ρ(fixa+1 y.λx.M )ρ (fixa+1 y.λx.N ) ⇓1 ρ (fixa+1 y.λx.N )an+1
Let V ≈CV .
τ1 W and ρ(M )[V /x][ρ(fix y.λx.M )/y] ⇓By induction hypothesis,aρ(fixa y.λx.M ) ≈C
τ1 →τ2 ρ (fix y.λx.N )Let ρ0 = ρ[V /x][ρ(fixa y.λx.M )/y] and ρ0 = ρ [W/x][ρ(fixa y.λx.N )/y].

We have ρ0 ≈CΓ,y:τ1 →τ2 ,x:τ1 ρ0 . By induction hypothesis,ρ0 (N ) ⇓Cn+τ2 +3 W 

a+1

a+1
and V  ≈Cy.λx.M ) ≈Cy.λx.N ).
τ2 W . Hence, ρ(fixτ1 →τ2 ρ (fix5Preservation of Execution TimeWe introduce the operational semantics proﬁling execution time and outline
the proof that the coercion interpretation of subtyping is also safe with respect
to execution time. The operational semantics for execution time is a simple
extension of the standard semantics as that for stack space. As the previous
section, we ﬁrst extend judgment of operational semantics to the following form:
M ⇓n Vwhere n represents execution time to evaluate M to V . For the rule of application
we use an auxiliary relation: V1 V2 ↓n V as before. The rules are given as follows.
1

V ⇓ V

M1 ⇓m V1 M2 [V1 /x] ⇓n V
let x = M1 in M2 ⇓m+n+1 V

M1 ⇓l V1 M2 ⇓m V2 V1 V2 ↓n V
M1 M2 ⇓l+m+n+1 V
M [V2 /x] ⇓n V
(λx.M )V2 ↓n V

M [V2 /x][fixk y.λx.M/y] ⇓n V
(fixk+1 y.λx.M )V2 ↓n V

All the rules are a straightforward extension of the standard rules.
Then it is shown that the conversion interpretation preserves execution timewithin a factor determined by the types appearing in a program.
Theorem 2. Let C[[∅  M : τ ]] = N and let C be an integer such that C > 7 σ
for all σ appearing in the derivation of ∅  M : τ . If M ⇓n V then N ⇓≤Cn W
for some W .
The factor of slowdown 7 σ is bigger than the factor of increase of stack space
σ . To prove this theorem, w use the method of logical relations which areindexed by a slowdown factor as well as a type. The relations V ≈C
τ W aredeﬁned as follows.
i ≈C
int i
V ≈C
bigint i
V ≈C
τ1 →τ2 W

V = i or V = in+1
V2
for all V1 ≈Cτ1 W1 , if V V1 ↓Cn+7τ1 →τ2 +1then W W1 ↓W2 and V2 ≈C
τ2 W2

The important diﬀerence from the relations for stack space is that slowdown of
the applications depends on the domain type τ1 as well as the range type τ2 ofa function type τ1 → τ2 .
With this deﬁnition, the main theorem is proved in the same manner as theproof for stack space. It is shown that a conversion function behaves well withrespect to the logical relations as before. Then the generalization of the main
theorem is proved by induction on the derivation of the conversion interpretationof a program.

6

Conclusions and Related Work

We have shown that conversion interpretation of subtyping preserves execution
time and stack space within a factor determined by the types in a program if
the subtyping relation is a partial order. Type-directed unboxing of Leroy isa translation similar to conversion interpretation of subtyping, but it does notpreserve execution time and stack space. This is because conversions of equivalent
types appear in type-directed unboxing.

We have considered only a very simple type system which does not include
product types and recursive types. We believe the results in this paper can beeasily extended for product types. However, our results cannot be extended forrecursive types. If we consider recursive types, cost of one application of coercion
cannot be bounded by a constant as Leroy discussed in his work on type-directed
unboxing for polymorphic languages [8]. Thus the conversion interpretation does
not preserve execution time nor stack space usage in the presence of subtyping
on recursive types.
We have shown that the conversion interpretation is safe with respect to timeand stack space by the method of logical relations. We believe the conversion
interpretation is also safe with respect to heap space, but it will be diﬃcult toadopt the same method for heap space. We have no idea how to formalize logicalrelations for heap space because the semantics proﬁling heap space is much more
complicated than those for time and stack space.
In the rest of this section I review other proof methods to show safety of
program transformations with respect to performance.
David Sands studied time safety of transformations for call-by-name languages [16, 15]. In his study he extended applicative bisimulation and its context lemma to account execution time. Applicative bisimulation with the context
lemma greatly simpliﬁes safety proofs of many program transformations. As withthe method of logical relations, it will be diﬃcult to extend this method if we
consider heap space or various extensions of languages.
Another approach is to analyze states of evaluation more directly, where
proofs are often based on induction on length of evaluation. Blelloch and Greiner
showed that an implementation of NESL based on an abstract machine preserves
execution time and space within a constant factor based on this approach [2]. Minamide showed that the CPS transformation preserves space within a constantfactor [9]. Gustavsson and Sands developed a theory of a space improvement relation for a call-by-need programming language [5, 6]. They clariﬁed their proofs
by considering evaluation of programs with holes based on a context calculus [17].
Bakewell and Runciman proposed an operational model for lazy functional programming languages based on graph rewriting [1]. As a proof method for themodel they considered an extension of bisimulation.

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

References[1] A. Bakewell and C. Runciman. A model for comparing the space usage of lazyevaluators. In Proceedings of the 2nd International ACM SIGPLAN Conference
on Principles and Practice of Declarative Programming, pages 151–162, 2000.

[2] G. E. Blelloch and J. Greiner. A provably time and space eﬃcient implementationof NESL. In Proceedings of the ACM SIGPLAN International Conference on
Functional Programming, pages 213–225, 1996.
[3] V. Breazu-Tannen, C. A. Gunter, and A. Scedrov. Computing with coercions. In
Proceedings of the 1990 ACM Conference on LISP and Functional programming,
pages 44–60, 1990.
[4] C. A. Gunter. Semantics of Programming Languages, chapter 4. The MIT Press,
1992.
[5] J. Gustavsson and D. Sands. A foundation for space-safe transformations of callby-need programs. In Proceedings of the Third International Workshop on Higher
Order Operational Techniques in Semantics (HOOTS99), volume 26 of ENTCS,
1999.
[6] J. Gustavsson and D. Sands. Possibilities and limitations of call-by-need space improvement. In Proceedings of the Sixth ACM SIGPLAN International Conference
on Functional Programming, pages 265–276, 2001.
[7] N. Heintze. Control-ﬂow analysis and type systems. In Proceedings of the 1995
International Static Analysis Symposium, volume 983 of LNCS, pages 189–206,
1995.
[8] X. Leroy. Unboxed objects and polymorphic typing. In the 19th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, pages 177–188,
1992.
[9] Y. Minamide. A space-proﬁling semantics of call-by-value lambda calculus andthe CPS transformation. In Proceedings of the Third International Workshop on
Higher Order Operational Techniques in Semantics (HOOTS99), volume 26 of
ENTCS, 1999.
[10] Y. Minamide. A new criterion for safe program transformations. In Proceedingsof the Forth International Workshop on Higher Order Operational Techniques in
Semantics (HOOTS), volume 41(3) of ENTCS, Montreal, 2000.
[11] Y. Minamide and J. Garrigue. On the runtime complexity of type-directed unboxing. In Proceedings of the Third ACM SIGPLAN International Conference on
Functional programming, pages 1–12, 1998.
[12] Y. Minamide, G. Morrisett, and R. Harper. Typed closure conversion. In Proceeding of the ACM Symposium on Principles of Programming Languages, pages
271–283, 1996.
[13] J. C. Mitchell. Foundations for Programming Languages, chapter 10. The MIT
Press, 1996.
[14] A. Ohori. A polymorphic record calculus and its compilation. ACM Transaction
on Programming Languages and Systems, 17(6):844–895, 1995.
[15] D. Sands. A naive time analysis and its theory of cost equivalence. Journal of
Logic and Computation, 5(4):495–541, 1995.
[16] D. Sands. Proving the correctness of recursion-based automatic program transformations. Theoretical Computer Science, 167(1&2):193–233, 1996.
[17] D. Sands. Computing with contexts: A simple approach. In Proceedings of theSecond Workshop on Higher-Order Operational Techniques in Semantics (HOOTS
II), volume 10 of ENTCS, 1998.