A Semantic Account of Type-Directed Partial Evaluation

Principles and Practice of Declarative Programming 1999, LNCS 1702

Andrzej Filinski^{⋆}

BRICS^{⋆⋆}, Dept. of Computer Science University of Aarhus, Denmark

                             andrzej@brics.dk

Abstract. We formally characterize partial evaluation of functional programs as a normalization problem in an equational theory, and derive a type-based normalization-by-evaluation algorithm for computing normal forms in this setting. We then establish the correctness of this algorithm using a semantic argument based on Kripke logical relations. For simplicity, the results are stated for a non-strict, purely functional language; but the methods are directly applicable to stating and proving correctness of type-directed partial evaluation in ML-like languages as well.

1 Introduction

The goal of partial evaluation (PE) is as follows: given a program ⊢ p : S×D→R of two arguments, and a fixed “static” argument s : S, produce a specialized program ⊢ p_{s} : D → R such that for all “dynamic” d : D, Eval(p_{s} d) = Eval(p(s, d)). That is, running the specialized program on the dynamic argument is equivalent to running the original program on both the static and the dynamic one.

In a functional language, it is of course trivial to come up with such a p_{s}: just take p_{s} = λd.p(s, d). That is, the specialized program simply invokes the original program with a constant first argument. But such a p_{s} is likely to be suboptimal: the knowledge of s may already allow us to perform some simplifications that are independent of d. For example, consider the power function:

power (n, x) =^{rec} if n = 0 then 1 else x × power(n − 1, x)

Suppose we want to compute the third power of several numbers. We can achieve this using the trivially specialized program:

power_{3} = λx.power(3, x)

But using a few simple rules derived from the semantics of the language, we can safely transform power_{3} to the much more efficient

power′_{3} = λx.x × (x × (x × 1))

⋆ Part of this work was carried out at the Laboratory for Foundations of Computer

Science, University of Edinburgh, supported by a EuroFOCS research fellowship. ⋆⋆ Basic Research in Computer Science (www.brics.dk),

Centre of the Danish National Research Foundation

Using further arithmetic identities, we can also easily eliminate the multiplication by 1. On the other hand, if only the argument x were known, we could not simplify much: the specialized program would in general still need to contain a recursive definition and a conditional test – in addition to the multiplication. (Note that, even when x is 0 or 1, the function as defined should still diverge for negative values of n.)

To facilitate automation of the task, partial evaluation is often expressed as a two-phase process, usually referred to as off-line PE [14]:

1. A binding-time annotation phase, which identifies all the operations that can be performed using just the static input. This can be done either mechanically by a binding-time analysis (often based on abstract interpretation), or – if the intended usage of the program is clear and the annotations are sufficiently intuitive and non-intrusive – as part of the original program.

2. A specialization phase, which takes the annotated program and the static input, and produces a simplified p_{s}, in which all the operations marked as static have been eliminated.

The annotations must of course be consistent, i.e., a subcomputation in the program cannot be classified as static if its result can not necessarily be found from only the static input. But they may be conservative by classifying some computations as dynamic even if they could in fact be performed at specialization time. Techniques for accurate binding-time analysis have been studied extensively [14]. In the following we will therefore limit our attention to the second phase, i.e., to efficiently specializing programs that are already binding-time separated.

A particularly simple way of phrasing specialization is as a general-purpose simplification of the trivially specialized program λd.p(s, d): contracting β-redexes and eliminating static operations as their inputs become known. What makes this approach attractive is the technique of “reduction-free normalization” or “normalization by evaluation”, already known from logic and category theory [2, 3, 7]. A few challenges arise, however, with extending these results to a programminglanguage setting. Most notably:

– Interpreted base types and their associated static operations. These need to be properly accounted for, in addition to the β-reduction.

– Unrestricted recursion. This prevents a direct application of the usual strongnormalization results. That is, not every well-typed term even has a normal form; and not every reduction strategy will find it when it does exist.

– Call-by-value languages, and effects other than non-termination. In such a setting, the usual βη-conversions are actually unsound: unrestricted rearrangement of side effects may completely change the meaning of a program.

We will treat the first two concerns in detail. The call-by-value case uses the same principles, but for space reasons we will only briefly outline the necessary changes.

The paper is organized as follows: Section 2 introduces our programming language, the notion of a binding-time separated signature, and our desiderata for a partial evaluator; Section 3 presents the type-directed partial evaluation algorithm; and Section 4 shows its correctness with respect to the criteria in Section 2.

Finally, Section 5 presents a few variations and extensions, and Section 6 concludes and outlines directions for further research.

2 A Small Language

2.1 The framework and one-level language

Our prototypical functional language has the following syntax of types and terms:

σ ::= b | σ_{1} → σ_{2}
E ::= l | c_{σ_{1},...,σ_{n}} | x | λx^{σ}.E | E_{1} E_{2}

Here b ranges over a set of base types listed in some signature Σ, l over a set Ξ(b) of literals (numerals, truth values, etc.) for each base type b, and c over a set of (possibly polymorphic) function constants in Σ. Adding finite-product types would be completely straightforward throughout the paper, but we omit this extension for conciseness.

A typing context Γ is a finite mapping of variable names to well-formed types over Σ. The typing rules for terms are then standard:

\frac{l ∈ Ξ(b)}{Γ ⊢_{Σ} l : b}  \frac{Σ(c_{σ_{1},...,σ_{n}}) = σ}{Γ ⊢_{Σ} c_{σ_{1},...,σ_{n}} : σ}  \frac{Γ (x) = σ}{Γ ⊢_{Σ} x : σ}

\frac{Γ, x: σ_{1} ⊢_{Σ} E : σ_{2}}{Γ ⊢_{Σ} λx^{σ_{1}}.E : σ_{1} → σ_{2}}  \frac{Γ ⊢_{Σ} E_{1} : σ_{1} → σ_{2}  Γ ⊢_{Σ} E_{2} : σ_{1}}{Γ ⊢_{Σ} E_{1} E_{2} : σ_{2}}

An interpretation of a signature Σ is a triple I = (B, L, C). B maps every base type b in Σ to a predomain (i.e., a bottomless cpo, usually discretely ordered). Then we can interpret every type phrase σ over Σ as a domain (pointed cpo):

[[b]]^{B} = B(b)_{⊥}
[[σ_{1} → σ_{2}]]^{B} = [[σ_{1}]]^{B} → [[σ_{2}]]^{B}

where the interpretation of an arrow type is the full continuous function space. We also define the meaning of a typing assignment Γ as a labelled product of the domains interpreting the types of individual variables,

[[Γ]]^{B} = ∏_{x∈dom Γ} [[Γ (x)]]^{B} .

Further, for any base type b and literal l ∈ Ξ(b), the interpretation must specify an element L_{b}(l) ∈ B(b); and for every type instance of a polymorphic constant, an element C(c_{σ_{1},...,σ_{n}}) ∈ [[Σ(c_{σ_{1},...,σ_{n}})]]^{B}. Then we interpret a welltyped term Γ ⊢_{Σ} E : σ as a (total) continuous function [[E]]^{I} : [[Γ]]^{B} → [[σ]]^{B},

[[l]]^{I}ρ = val^{⊥} L_{b}(l)
[[c_{σ_{1},...,σ_{n}}]]^{I}ρ = C(c_{σ_{1},...,σ_{n}})
[[x]]^{I}ρ = ρx
[[λx^{σ}.E]]^{I}ρ = λa^{[[σ]]^{B}}.[[E]]^{I}(ρ[x ↦ a])
[[E_{1} E_{2}]]^{I}ρ = [[E_{1}]]^{I}ρ([[E_{2}]]^{I}ρ)

(We use the following notation: val^{⊥} x and let^{⊥} y ⇐ x in f y are lifting-injection and the strict extension of f, respectively; b→x[]y chooses between x and y based on the truth value b.)

When ⊢_{Σ} E : b is a closed term of base type, we define the partial function Eval_{I} by Eval_{I}(E) = n if [[E]]^{I}∅ = val^{⊥} n and undefined otherwise.

Definition 1 (standard static language). We define a simple functional language (essentially PCF [17]) by taking the signature Σ_{s} as follows. The base types are int and bool; the literals, Ξ(int) = {…, -1, 0, 1, 2, … } and Ξ(bool) = {true, false}; and the constants,

+, −, × : int → int → int
=, < : int → int → bool

if_{σ} : bool → σ → σ → σ
fix_{σ} : (σ → σ) → σ

(We write the binary operations infixed for readability.) The interpretation of this signature is also as expected:

B_{s}(bool) = B = {tt, ff }
B_{s}(int) = Z = {…, −1, 0, 1, 2, … }
C_{s}(⋆) = λx^{Z_{⊥}}.λy^{Z_{⊥}}.let^{⊥} n ⇐ x in let^{⊥} m ⇐ y in val^{⊥} m ⋆ n ⋆∈{+,−,×,=,<}
C_{s}(if_{σ}) = λx^{B_{⊥}}.λa_{1}^{[[σ]]}.λa_{2}^{[[σ]]}.let^{⊥} b ⇐ x in b → a_{1} [] a_{2}
C_{s}(fix_{σ}) = λf^{[[σ]]→[[σ]]}.⨆_{i∈ω} f^{i} ⊥_{[[σ]]}

It is well known (computational adequacy of the denotational semantics for call-by-name evaluation [17]) that with this interpretation, Eval_{I_{s}} is computable.

2.2 The binding-time separated language

Assume now that the signature Σ is partitioned according to binding times, Σ = Σ_{s}, Σ_{d}. We will write type and term constants from the static part overlined, and the dynamic ones underlined. For simplicity, we require that the dynamic base types do not come with any new literals, i.e., Ξ(\underline{b}) = ∅. (If needed, they can be added as dynamic constants.) However, some base types will be persistent, i.e., have both static and dynamic versions with the same intended meaning. In that case, we also include lifting functions $_{b} : \overline{b} → \underline{b} in the dynamic signature.

We say that a type τ is fully dynamic if it is constructed from dynamic base types only,

τ ::= \underline{b} | τ_{1} → τ_{2}

We also reserve Δ for typing assumptions assigning fully dynamic types to all variables. All term constants in Σ_{d} must have fully dynamic types, and in particular, polymorphic dynamic constants must only be instantiated by dynamic types, e.g., Σ_{d}(\underline{if}_{τ}) = \underline{bool} → τ → τ → τ.

We will always take the language from Definition 1 with the standard semantics I_{s} as the static part. The dynamic signature typically also has some intended evaluating interpretation I_{d}^{e}; in particular, when Σ_{d} is merely a copy of Σ_{s}, we can use I_{s} directly for I_{d}^{e} (interpreting all lifting functions as identities). Later, however, we will also introduce a “code-generating”, residualizing interpretation.

Example 1. Here are the four different binding-time annotations for the function power : int → int → int (abbreviating int as ι):

power_{ss} : \overline{ι} → \overline{ι} → \overline{ι} = λx\overline{ι}.\overline{fix}_{\overline{ι}→\overline{ι}} (λp^{\overline{ι}→\overline{ι}}.λn\overline{ι}.\overline{if}\overline{ι} (n \overline{=} 0) 1 (x \overline{×} p(n \overline{−} 1)))
power_{sd} : \overline{ι} → \underline{ι} → \underline{ι} = λx\overline{ι}.\underline{fix}_{\underline{ι}→\underline{ι}} (λp^{\underline{ι}→\underline{ι}}.λn\underline{ι}.\underline{if}\underline{ι} (n \underline{=} $ 0)($ 1)($ x \underline{×} p(n \underline{−} $ 1)))
power_{ds} : \underline{ι} → \overline{ι} → \underline{ι} = λx\underline{ι}.\overline{fix}_{\overline{ι}→\underline{ι}} (λp^{\overline{ι}→\underline{ι}}.λn\overline{ι}.\overline{if}\underline{ι} (n \overline{=} 0)($ 1)(x \underline{×} p(n \overline{−} 1)))
power_{dd} : \underline{ι} → \underline{ι} → \underline{ι} = λx\underline{ι}.\underline{fix}_{\underline{ι}→\underline{ι}} (λp^{\underline{ι}→\underline{ι}}.λn\underline{ι}.\underline{if}\underline{ι} (n \underline{=} $ 0)($ 1)(x \underline{×} p(n \underline{−} $ 1)))

Note how the fixed-point and conditional operators are classified as static or dynamic, depending on the binding time of the second argument.

2.3 Static normal forms and PE

Definition 2 (static normal forms). Among the well-typed, purely dynamic terms Δ ⊢_{Σ_{d}} E : τ, we distinguish those in normal and atomic form:

\frac{Δ ⊢^{at} E : \underline{b}}{Δ ⊢^{nf} E : \underline{b}}  \frac{Δ, x: τ_{1} ⊢^{nf} E : τ_{2}}{Δ ⊢^{nf} λx^{τ_{1}}.E : τ_{1} → τ_{2}} x∉dom Δ

\frac{l ∈ Ξ(\overline{b})}{Δ ⊢^{at} $_{b} l : \underline{b}}  \frac{Σ_{d}(\underline{c}_{τ_{1},...,τ_{n}}) = τ}{Δ ⊢^{at} \underline{c}_{τ_{1},...,τ_{n}} : τ}  \frac{Δ(x) = τ}{Δ ⊢^{at} x : τ}

\frac{Δ ⊢^{at} E_{1} : τ_{1} → τ_{2} Δ ⊢^{nf} E_{2} : τ_{1}}{Δ ⊢^{at} E_{1} E_{2} : τ_{2}}

In particular, such terms contain no static constants nor β-redexes. (Incidentally, this also means that if we had included polymorphic lets in the source language, they would simply get unfolded in the resulting normal forms.)

We can now define a notion of normalization based on (undirected) equality, rather than on (directed) reduction [3]. Since lambda-abstracting a dynamic-type term over a dynamic-type variable still yields a dynamic term, it suffices to be able to compute normal forms of closed terms:

Definition 3 (static equivalence and normalization). Let I_{s} be an interpretation of Σ_{s}. We say that two terms ⊢_{Σ_{s},Σ_{d}} E : σ and ⊢_{Σ_{s},Σ_{d}} E′ : σ are statically equivalent wrt. I_{s}, written E =^{I_{s}} E′, if for all I_{d} interpreting Σ_{d}, [[E]]^{I_{s},I_{d}} = [[E′]]^{I_{s},I_{d}}. A static-normalization function is then a computable partial function NF on well-typed terms such that

1. If ⊢_{Σ_{s},Σ_{d}} E : τ and NF (E) = Ẽ then ⊢_{Σ_{d}}^{nf} Ẽ : τ and Ẽ =^{I_{s}} E.

2. If also ⊢_{Σ_{s},Σ_{d}} E′ : τ and E′ =^{I_{s}} E then NF (E′) ≡ NF (E) (α-equivalence).

We further say that such a normalization function is complete if whenever an Ẽ satisfying the conditions in (1) exists, NF (E) is defined.

Example 2. One can check that a complete static-normalization function NF for our language must have the following properties:

NF ($ (power_{ss} 3 4)) ≡ $ 81
NF (λx\underline{int}.power_{ds} x 3) ≡ λx\underline{int}.x \underline{×} (x \underline{×} (x \underline{×} $ 1))
NF (λx\underline{int}.power_{ds} x -2) undefined

Note first that ordinary evaluation is just a special case of static normalization. The second example shows how static normalization achieves the partialevaluation goal of the introduction. Finally, some terms have no static normal form at all; in that case, the normalization function must diverge.

There are two basic ways to compute normal forms. The usual one is based on term rewriting, repeatedly locating and contracting β-redexes and applications of static constants (and possibly η-expanding the final result). But there is an alternative technique, normalization by evaluation, which utilizes the existing mechanism of complete-program evaluation (defined only for closed terms of base type) as the normalization engine for general terms. This is the subject of the next section.

3 A Normalization-by-Evaluation Algorithm

We now present Type-Directed Partial Evaluation (TDPE), an efficient algorithm for computing static normal forms.

3.1 Representing programs as data

To compute normal forms, we need a way of representing them as program outputs. Assume therefore that we have base cpos rich enough to contain unique representations of all well-formed dynamic types, variable names, and (open) static-normal form terms, i.e., sets T, V, and Λ with injective operations

BASE_{b} : T
ARR : T × T → T
LIT_{b} : B_{s}(b) → Λ

CST : V × T^{∗} → Λ
VAR : V → Λ
LAM : V × T × Λ → Λ
APP : Λ × Λ → Λ

(where T^{∗} is the set of finite lists of elements from T). Using these, we can define injective representation functions for types and terms, such that ^{⌜}τ^{⌝} ∈ T for any dynamic type τ, and ^{⌜}E^{⌝} ∈ Λ for Δ ⊢_{Σ_{d}}^{nf} E : τ, by equations such as

⌜τ_{1}→τ_{2}^{⌝} = ARR(^{⌜}τ_{1}^{⌝},^{⌜}τ_{2}^{⌝})  ^{⌜}λx^{τ} .E^{⌝} = LAM (x,^{⌜}τ^{⌝},^{⌜}E^{⌝})  ^{⌜}$_{b} l^{⌝} = LIT_{b}(L_{b}(l))

We do not need to require a priori that all elements of T and Λ represent wellformed types and terms (although this is easy to achieve), let alone well-typed ones, or ones in normal form. For example, we could simply take all of T, V, and Λ as the type of finite character strings. Or, even more radically, Gödel-code everything in terms of integer arithmetic only.

To account for potentially diverging normalizations, we must now turn the set of term representations into a pointed cpo. To also model the generation of “new” variable names, however, we will not work with elements of Λ_{⊥} directly, but instead introduce a term-family representation,

Λ̂ = N → Λ_{⊥}

where N ⊆ N. The intent is that for e ∈ Λ̂ and i ∈ N, if ei = val^{⊥} ^{⌜}E^{⌝} then all bound variables of E will belong to the set {g_{i}, g_{i+1}, … } ⊆ V.

We also define wrapper functions to conveniently build representations of lambda-terms without committing to particular choices of bound-variable names:

L̂IT_{b} : B_{s}(b) → Λ̂ = λn. λi. val^{⊥} LIT_{b}(n)
{ \atop CST} : V × T^{∗} → Λ̂ = λ(c, t). λi. val^{⊥} CST (c, t)
{ \atop VAR} : V → Λ̂ = λv. λi. val^{⊥} VAR(v)
{ \atop LAM} : T × (V → Λ̂) → Λ̂ = λ(t, ε). λi. let^{⊥} l ⇐ εg_{i} (i + 1) in val^{⊥} LAM (g_{i}, t, l)
{ \atop APP} : Λ̂ × Λ̂ → Λ̂ =
λ(e_{1}, e_{2}). λi. let^{⊥} l_{1} ⇐ e_{1} i in let^{⊥} l_{2} ⇐ e_{2} i in val^{⊥} APP(l_{1}, l_{2})

(These definitions would not be needed in a setting with support for higher-order abstract syntax. But one of our goals is to show rigorously that all the variablename manipulations can be done efficiently by the normalization algorithm itself, without relying on higher-level operations such as capture-avoiding substitution or higher-order matching.)

Example 3. Let t = ARR(BASE_{int}, BASE_{int}). Then

{ \atop LAM} (t, λv^{V}.{ \atop APP} ({ \atop VAR} v, L̂IT_{int} 3))7
= val^{⊥} LAM (g_{7}, t, APP(VAR(g_{7}), LIT_{int}(3))) = val^{⊥} ^{⌜}λg_{7}^{\underline{int}→\underline{int}}.g_{7} ($ 3)^{⌝}

That is, we can apply an element of Λ̂ constructed using the wrapper functions to a starting index and obtain the representation of a concrete lambda-term.

3.2 The residualizing interpretation

We now define a non-standard interpretation I_{d}^{r} = (B_{d}^{r}, ∅, C_{d}^{r}) of the dynamic signature Σ_{d}, based on representations of syntactic program fragments and operations constructing such representations. We will abbreviate [[−]]^{I_{s},I_{d}^{r}} as [[−]]_{r}. For the interpretation of Σ_{d}’s types, we take

B_{d}^{r}(\underline{b}) = Λ̂.

This allows us to define for any dynamic τ a pair of continuous functions, often called reification, ↓^{τ} : [[τ]]_{r} → Λ̂, and reflection, ↑_{τ} : Λ̂ → [[τ]]_{r}, as follows:

↓^{\underline{b}} = λtΛ̂.t  ↓^{τ_{1}→τ_{2}} = λf^{[[τ_{1}]]_{r}→[[τ_{2}]]_{r}}.{ \atop LAM} (^{⌜}τ_{1}^{⌝}, λv^{V}.↓^{τ_{2}} (f (↑_{τ_{1}} ({ \atop VAR} v))))
↑\underline{b} = λeΛ̂.e  ↑_{τ_{1}→τ_{2}} = λeΛ̂.λa^{[[τ_{1}]]_{r}}.↑_{τ_{2}} ({ \atop APP} (e, ↓^{τ_{1}} a))

Informally, reification constructs a syntactic representation of a “well-behaved” semantic value, while reflection constructs such values from pieces of syntax. For the residualizing interpretations of Σ_{d}’s term constants we now take

C_{d}^{r}(\underline{c}_{τ_{1},...,τ_{n}}) = ↑_{Σ_{d}(c_{τ_{1},...,τn})} ({ \atop CST} (c, [^{⌜}τ_{1}^{⌝}, …,^{⌜}τ_{n}^{⌝}]))
C_{d}^{r}($_{b}) = λx^{B_{s}(b)_{⊥}}.let^{⊥} n ⇐ x in L̂IT_{b} n

That is, a general dynamic constant is simply interpreted as the reflection of its type-annotated name, while a lifting function forces evaluation of its argument and constructs a representation of the literal result. (It is this forcing of static subcomputations that may cause the whole specialization process to diverge.)

Example 4. Applying the reification function to the residualizing meaning of a term not in static normal form, we obtain:

↓^{(\underline{int}→\underline{int})→\underline{int}} ([[(λx\overline{int}.λf^{\underline{int}→\underline{int}}.f ($_{int} (x \overline{+} 1))) 2]]_{r} ∅)
= ↓^{(\underline{int}→\underline{int})→\underline{int}} ([[λf.f ($_{int} (x \overline{+} 1))]]_{r} (∅[x ↦ [[2]]_{r} ∅]))
= ↓^{(\underline{int}→\underline{int})→\underline{int}} (λφ^{Λ̂→Λ̂}.[[f ($_{int} (x \overline{+} 1))]]_{r} (∅[x ↦ val^{⊥} 2, f ↦ φ]))
= ↓^{(\underline{int}→\underline{int})→\underline{int}} (λφ.φ(C_{d}^{r}($_{int})(C_{s}(+)(val^{⊥} 2)(val^{⊥} 1))))
= ↓^{(\underline{int}→\underline{int})→\underline{int}} (λφ.φ(C_{d}^{r}($_{int})(val^{⊥} 3))) = ↓^{(\underline{int}→\underline{int})→\underline{int}} (λφ.φ(L̂IT_{int} 3))
= { \atop LAM} (^{⌜}\underline{int} → \underline{int}^{⌝}, λv^{V}.↓^{\underline{int}}((λφ.φ(L̂IT_{int} 3))(↑_{\underline{int}→\underline{int}} ({ \atop VAR} v))))
= { \atop LAM} (ARR(BASE_{int}, BASE_{int}), λv^{V}.{ \atop APP} ({ \atop VAR} v)(L̂IT_{int} 3))

And applying this value to 7 as the first bound-variable index gives us precisely the normal-form term from Example 3 at the end of the previous section.

3.3 The algorithm

So far, we have looked at a semantic property: from the interpretation of a lambdaterm in a non-standard denotational semantics of the dynamic signature, we can apparently recover that term’s normal form. But this semantic result also forms the basis of an eminently practical normalization algorithm, obtained by pulling back the components of the residualizing semantics to the level of program syntax.

We say that a realization Φ of a signature Σ in a programming language given by Σ_{pl} is a substitution assigning to every type constant of Σ, a type over Σ_{pl}, and to every term constant of Σ, a Σ_{pl}-term. (For simplicity, we assume that the literals of Σ’s base types are also literals of the corresponding Σ_{pl}-types.)

Suppose now that Σ_{s} ⊆ Σ_{pl}, I_{pl} agrees with I_{s}, and Σ_{pl} also has some distinguished base types typ and exp with B_{pl}(typ) = T and B_{pl}(exp) = Λ, as well as the associated (strict) constructor constants. Note that [[int → exp]] = Λ̂ (with N = Z_{⊥}). Then we can realize the base types of (Σ_{s}, Σ_{d}) in Σ_{pl} by

Φ^{r}(\overline{b}) = b Φ^{r}(\underline{b}) = int → exp

so that [[σ{Φ^{r}}]]^{B_{pl}} = [[σ]]_{r}. Further, for any τ, we can define closed Σ_{pl}-terms,

name_{τ} : typ  reify_{τ} : τ{Φ^{r}} → int → exp  reflect_{τ} : (int → exp) → τ{Φ^{r}}

such that [[name_{τ}]]^{I_{pl}}∅ = val^{⊥} ^{⌜}τ^{⌝}, [[reify_{τ}]]^{I_{pl}}∅ = ↓^{τ}, and [[reflect_{τ}]]^{I_{pl}}∅ = ↑_{τ}. And using those, we can define realizations of the term constants from (Σ_{s}, Σ_{d}):

Φ^{r}(\overline{c}_{σ_{1},...,σ_{n}}) = c_{σ_{1}\{Φ^{r}\},...,σ_{n}\{Φ^{r}\}}
Φ^{r}(\underline{c}_{τ_{1},...,τ_{n}}) = reflect_{Σ_{d}(\underline{c}_{τ_{1},...,τn})} (λi.CST(c, [name_{τ_{1}}, …, name_{τ_{n}}]))
Φ^{r}($_{b}) = λn.λi.LIT_{b} n (given C_{pl}(LIT_{b}) = λx.let^{⊥} n ⇐ x in val^{⊥} LIT_{b}(n))

so that [[E{Φ^{r}}]]^{I_{pl}} = [[E]]_{r}. Note in particular that the realizations of static base types and constants are exactly the corresponding constructs from the programming language. This means that we can even use the usual syntactic sugar (such as letrec for applications of \overline{fix}) in the static parts of programs to be specialized.

We can use this realization to express our normalization algorithm:

Definition 4 (TDPE). For any dynamic type τ, we define the partial function TDPE_{τ} : {E | ⊢_{Σ_{s},Σ_{d}} E : τ} ⇀ {E | ⊢_{Σ_{d}}^{nf} E : τ} by

TDPE_{τ} (E) = Ẽ if Eval_{I_{pl}}(reify_{τ} E{Φ^{r}} 0) = ^{⌜}Ẽ^{⌝} .

This TDPE is clearly computable; we will show in Section 4 that it is indeed a complete static-normalization function.

Note that we can view TDPE an instance of “cogen-based specialization” [13], in which a “compiler generator” is used to syntactically transform a (binding-time annotated) program ⊢ p : S × D → R into its generating extension ⊢ p^{†} : S → exp, with the property that for any s : S, Eval(p^{†} s) = ^{⌜}p_{s}^{⌝}. That is, we effectively take

p^{†} = λs^{S}.reify_{D→R} (λd^{D}.p{Φ^{r}}(s, d))0 .

TDPE shares the general high efficiency of cogen-based PE [12]. Formulating the task in terms of static normalization over a binding-time separated signature, however, permits a very precise yet concise syntactic characterization of the specialized program p_{s}. Also, unlike traditional cogens, TDPE does not require any binding-time annotation of lambdas and applications in the source program.

As a further advantage, the signatures and realizations can be very conveniently expressed in terms of parameterized modules in a Standard ML-style module system. The program to be specialized is simply written as the body of a functor parameterized by the signature of dynamic operations. The functor can then be applied to either an evaluating (Φ^{e}) or a residualizing (Φ^{r}) structure. That is, the cogen pass does not even require an explicit syntactic traversal of the program, making it possible to enrich the static fragment of the language (e.g., with pattern matching) without any modification to the partial evaluator itself.

It is also worth noting that the τ-indexed families above can be straightforwardly defined even in ML’s type system: consider the type abbreviation

tdpe(α) ≡ typ × (α → int → exp) × ((int → exp) → α) .

Then for any dynamic type τ, we can construct a term of type tdpe(τ{Φ^{r}}) whose value is the triple (name_{τ} , reify_{τ} , reflect_{τ}). We do this by defining once and for all two ML-typable terms

base : tdpe(int → exp) arrow : ∀α, β. tdpe(α) × tdpe(β) → tdpe(α → β) , with which we can then systematically construct the required value. The technique is explained in more detail elsewhere [18].

Finally, the dynamic polymorphic constants (e.g., \underline{fix}) now take explicit representations of the types at which they are being instantiated as extra arguments. In the evaluating realization, these extra arguments are ignored; but the residualizing realization uses them to construct the name-reflect-reify triple for Σ(\underline{c}_{τ_{1},...,τ_{n}}) given corresponding triples for τ_{1}, …, τ_{n}.

3.4 Applications

Despite its apparent simplicity, TDPE has been successfully used for several nontrivial examples; see Danvy’s tutorial for an overview [6]. Many of these actually use the slightly more complicated call-by-value version [4] (see Section 5.4). Because it exploits the highly-optimized evaluation mechanism of a functional language, such a partial evaluator is typically much faster than one representing and manipulating the source program as an explicit value.

Let us just mention here that in addition to stand-alone, source-to-source PE, the TDPE framework can be particularly naturally employed as a “semantic backend” for executable language specifications. That is, if we explicitly parameterize such a specification by the signature of runtime operations (including conditionals, fixed points, etc.), we can instantiate this signature with either the runtime realization, yielding an interpreter, or with the residualizing signature, yielding a compiler [8, 11]. Amusingly, the specializer does not even need the actual text of the specification, only its representation as an already compiled module.

4 Showing Correctness

In this section, we sketch a correctness proof for the TDPE algorithm, i.e., that it computes static normal forms when they exist. For the case without static constants, essentially the same algorithm can actually be extracted directly from the standard (syntactic) proof of strong normalization for the simply typed lambdacalculus [1]; but it is not clear if this approach can be extended to a richer programming-language setting.

Instead, our proof uses the technique of semantic logical relations, structured similarly to Gomard and Jones’s proof of Lambda-mix [14, 8.8], but accounting more rigorously for potential divergence and for the generation of “fresh” variable names. It also admits a richer type structure for the dynamic language. (We can still treat the untyped variant as a special case; see Section 5.1.)

4.1 Properties of the term-family representation

Let some evaluating dynamic interpretation I_{d}^{e} of Σ_{d} be given. We abbreviate [[−]]^{I_{s},I_{d}^{e}} as [[−]]_{e} (and [[−]]^{I_{s},I_{d}^{r}} as [[−]]_{r} as before).

Definition 5 (partial meaning relation, ≻). For any Δ, let

♯Δ = max({i + 1 | g_{i} ∈ dom Δ} ∪ {0})

(so if i ≥ ♯Δ then g_{i} ∉ dom Δ). Then for any Δ, τ, s ∈ {nf, at} (as used in Definition 2), δ ∈ [[Δ]]^{I_{d}^{e}}, e ∈ Λ̂, and a ∈ [[τ]]^{I_{d}^{e}}, we define a relation by

e @^{Δ} δ ≻_{τ}^{s} a ⟺ ∀i ≥ ♯Δ. ei = ⊥ ∨ ∃E. ei = val^{⊥} ^{⌜}E^{⌝} ∧ Δ ⊢_{Σ_{d}}^{s} E : τ ∧ [[E]]^{I_{d}^{e}}δ = a

This roughly expresses that “[[e]]δ = a”, but taking into account variable renaming, partiality, and simplification: for all sufficiently large starting indices i, if e i converges, it must represent a normal-form term with the right meaning. We check that this relation is semantically well behaved:

Definition 6 (admissibility). We say that a relation R ⊆ A × A′ between two pointed cpos is admissible (or inclusive) if it is chain-complete (i.e., for all chains (a_{i})_{i} and (a′_{i})_{i}, if ∀i. (a_{i}, a′_{i}) ∈ R then also (⨆_{i} a_{i}, ⨆_{i} a′_{i}) ∈ R) and pointed (i.e., (⊥_{A}, ⊥_{A′}) ∈ R).

Lemma 1 (≻ is admissible). For any Δ, δ ∈ [[Δ]]^{I_{d}^{e}}, τ, and s ∈ {nf, at}, the relation {(e, a) | e @^{Δ} δ ≻_{τ}^{s} a} is admissible.

Proof. Straightforward, noting that admissible relations are closed under arbitrary intersection, and that any chain in Λ_{⊥} is eventually constant. ⊓ ⊔

Although the output of TDPE is a closed program, we still need to account for the typing and meaning of open program fragments as they are being constructed and put into context:

Definition 7 (Kripke structure). A world is a pair (Δ, δ) where δ ∈ [[Δ]]^{I_{d}^{e}}. Such worlds are partially ordered by

(Δ′, δ′) ≥ (Δ, δ) ⟺ ∀x ∈ dom Δ. Δ′(x) = Δ(x) ∧ δ′ x = δ x

Lemma 2 (≻ is Kripke). If e @^{Δ} δ ≻_{τ}^{s} a and (Δ′, δ′) ≥ (Δ, δ), then also e @^{Δ′} δ′ ≻_{τ}^{s} a.

Proof. Follows easily from standard weakening properties of the typing relation (if Δ ⊢ E : τ then Δ′ ⊢ E : τ) and denotational semantics ([[E]]δ′ = [[E]]δ). ⊓ ⊔

Lemma 3 (meanings of term families). The wrapper functions have the following properties:

1. If Δ(v) = τ then { \atop VAR} v @^{Δ} δ ≻_{τ}^{at} δ v.

2. If n ∈ B_{s}(b) then L̂IT_{b} n @^{Δ} δ ≻at ; \underline{b} val^{⊥} n

3. { \atop CST} (c, [^{⌜}τ_{1}^{⌝}, …,^{⌜}τ_{n}^{⌝}]) @^{Δ} δ ≻_{Σ_{d}(\underline{c}_{τ_{1},...,τn})}^{at} C_{d}^{e}(\underline{c}_{τ_{1},...,τ_{n}})

4. If for all v ∉ dom Δ and a ∈ [[τ_{1}]]^{I_{d}^{e}}, εv @^{Δ,v:τ_{1}} δ[v ↦ a] ≻_{τ_{2}}^{nf} f a

then { \atop LAM} (^{⌜}τ_{1}^{⌝}, ε) @^{Δ} δ ≻_{τ_{1}→τ_{2}}^{nf} f.

5. If e_{1} @^{Δ} δ ≻_{τ_{1}→τ_{2}}^{at} f and e_{2} @^{Δ} δ ≻_{τ_{1}}^{nf} a then { \atop APP} (e_{1}, e_{2}) @^{Δ} δ ≻_{τ_{2}}^{at} f a

Proof. Straightforward verification in all cases. (For case 4, we exploit the fact that [[τ_{1}]]^{I_{d}^{e}} is always non-empty; this shortcut can be avoided by using a slightly more complicated world structure throughout the proof.) ⊓ ⊔ 4.2 Soundness of TDPE

We prove soundness by formally relating the standard and the residualizing interpretations of types and terms.

Definition 8 (logical relation, ∼_{σ}). For any type σ and world (Δ, δ), we define a relation a @^{Δ} δ ∼_{σ} a′, where a ∈ [[σ]]_{r} and a′ ∈ [[σ]]_{e} by:

n @^{Δ} δ ∼\overline{b} n′ ⟺ n = n′
e @^{Δ} δ ∼\underline{b} n′ ⟺ e @^{Δ} δ ≻nf ; \underline{b} n′
f @^{Δ} δ ∼_{σ_{1}→σ_{2}} f′ ⟺ ∀(Δ′, δ′) ≥ (Δ, δ).
∀a, a′. a @^{Δ′} δ′ ∼_{σ_{1}} a′ ⇒ f a @^{Δ′} δ′ ∼_{σ_{2}} f′ a′

We first check the standard requirements:

Lemma 4 (∼_{σ} is admissible). For any σ, the relation {(a, a′) | a @^{Δ} δ ∼_{σ} a′} is admissible.

Proof. Simple induction on σ. For \underline{b}, use admissibility of ≻ (Lemma 1). ⊓ ⊔

Lemma 5 (∼_{σ} is Kripke). If e @^{Δ} δ ∼_{σ} a and (Δ′, δ′) ≥ (Δ, δ), then also e @^{Δ′} δ′ ∼_{σ} a.

Proof. This is a standard result about Kripke logical relations; the proof is by a simple induction on σ, using Lemma 2 for the base case σ = \underline{b}. ⊓ ⊔

We obtain our main correctness result from two lemmas:

Lemma 6 (soundness, type part). For any dynamic type τ,

1. If a @^{Δ} δ ∼_{τ} a′ then ↓^{τ} a @^{Δ} δ ≻_{τ}^{nf} a′.

2. If e @^{Δ} δ ≻_{τ}^{at} a′ then ↑_{τ} e @^{Δ} δ ∼_{τ} a′.

Proof. Straightforward induction on τ, using the properties of the wrapper functions from Lemma 3. ⊓ ⊔

Lemma 7 (soundness, term part). Let (Δ, δ) be a world, and let ρ ∈ [[Γ]]_{r} and ρ′ ∈ [[Γ]]_{e}. Then for any well-typed term Γ ⊢_{Σ_{s},Σ_{d}} E : σ, if ∀x ∈ dom Γ. ρx @^{Δ} δ ∼_{Γ (x)} ρ′ x then [[E]]_{r} ρ @^{Δ} δ ∼_{σ} [[E]]_{e} ρ′.

Proof. This is the usual Kripke logical relations lemma, proved by straightforward induction on E. The only non-standard case is that of E = \underline{c}_{τ_{1},...,τ_{n}}, for which we need Lemma 6(2). For E = \overline{fix}_{σ}, we use fixed-point induction, i.e., Lemma 4 together with the chain-based construction of C_{s}(fix_{σ}) in Definition 1. ⊓ ⊔

Theorem 1 (soundness). TDPE is a static-normalization function.

Proof. Observe first that T DP E_{τ} (E) = Ẽ iff ↓^{τ} ([[E]]_{r} ∅)0 = val^{⊥} ^{⌜}Ẽ^{⌝}. Now, by Lemma 7, since empty environments are vacuously related, [[E]]_{r} ∅ @ ∅ ∼_{τ} [[E]]_{e} ∅. And thus by Lemma 6(1), ↓^{τ} ([[E]]_{r} ∅) @ ∅ ≻_{τ}^{nf} [[E]]_{e} ∅, which, by the definitions of ≻_{τ} and ♯, gives us precisely that ⊢_{Σ_{d}}^{nf} Ẽ : τ and [[Ẽ]]^{I_{d}^{e}} = [[E]]^{I_{s},I_{d}^{e}}.

For the second part, if E′ =^{I_{s}} E then in particular [[E′]]_{r} = [[E]]_{r}. And thus by the observation above, we must have TDPE_{τ} (E′) = TDPE_{τ} (E). ⊓ ⊔ 4.3 Completeness of TDPE

To supplement the above partial-correctness result, we can also show that if a suitable Ẽ exists, the algorithm will actually find it. This proof uses a much simpler logical-relation argument, capturing the intuition that the algorithm necessarily converges when applied to a term containing no static constants:

Definition 9 (totality predicate). For any dynamic type τ, we define a predicate T_{τ} ⊆ [[τ]]^{I_{d}^{r}} by

T\underline{b} = \{e ∈ Λ̂ | ∀i. ei ≠ ⊥\}
T_{τ_{1}→τ_{2}} = {f ∈ [[τ_{1}]]^{I_{d}^{r}} → [[τ_{2}]]^{I_{d}^{r}} | ∀a ∈ T_{τ_{1}}. fa ∈ T_{τ_{2}}}

As before, we then obtain the result from two main lemmas:

Lemma 8 (completeness, type part). For any dynamic type τ,

1. If a ∈ T_{τ} then for all i ≥ 0, ↓^{τ} a i ≠ ⊥.

2. If for all i ≥ 0, ei ≠ ⊥ then ↑_{τ} e ∈ T_{τ}.

Proof. Straightforward induction on τ, by inspection of the definitions of the wrapper functions. ⊓ ⊔

Lemma 9 (completeness, term part). Let δ ∈ [[Δ]]^{I_{d}^{r}}. Then for any well-typed term Δ ⊢_{Σ_{d}} E : τ, if ∀x ∈ dom Δ. δ x ∈ T_{Δ(x)} then [[E]]^{I_{d}^{r}}δ ∈ T_{τ}.

Proof. Standard induction on E, using Lemma 8(2) for dynamic constants. ⊓ ⊔

Theorem 2 (completeness). TDPE is a complete static-normalization function.

Proof. Suppose ⊢_{Σ_{s},Σ_{d}} E : τ has the static normal form ⊢_{Σ_{d}} Ẽ : τ. Then in particular [[E]]_{r} = [[E]]^{I_{s},I_{d}^{r}} = [[Ẽ]]^{I_{d}^{r}}. By Lemma 9, [[Ẽ]]^{I_{d}^{r}}∅ ∈ T_{τ}, and thus by Lemma 8(1), ↓^{τ} ([[E]]_{r} ∅)0 = ↓^{τ} ([[Ẽ]]^{I_{d}^{r}} ∅)0 ≠ ⊥, so TDPE_{τ} (E) is defined. ⊓ ⊔

5 Variations and Extensions

5.1 Lambda-mix

We can use the previous results to show correctness of partial evaluation for languages like the one used for Lambda-mix [14, 8.8]. Here, the dynamic language is untyped. Or, more precisely, it has a single type \underline{d} of dynamic values, and operators:

\frac{Γ, x: \underline{d} ⊢ E : \underline{d}}{Γ ⊢ \underline{λ}x. E : \underline{d}}  \frac{Γ ⊢ E_{1} : \underline{d}  Γ ⊢ E_{2} : \underline{d}}{Γ ⊢ E_{1} \underline{@} E_{2} : \underline{d}}

To model this in our typed framework, we let the dynamic signature Σ_{d} contain the single base type \underline{d}, and constants \underline{ϕ} : (\underline{d} → \underline{d}) → \underline{d} and \underline{ψ} : \underline{d} → \underline{d} → \underline{d}. We can then treat dynamic lambda-abstraction and application as abbreviations:

\underline{λ}x. E ≡ \underline{ϕ}(λx\underline{d}.E)  and  E_{1} \underline{@} E_{2} ≡ \underline{ψ} E_{1} E_{2}

In the evaluating dynamic semantics I_{d}^{e} of Σ_{d}, the type constant \underline{d} is interpreted as a solution to the domain equation

D ≅ (D → D) ⊕ Z_{⊥} ⊕ B_{⊥} ,

and \underline{ϕ} and \underline{ψ} as the evident embedding and projection functions for the first summand. In the residualizing interpretation I_{d}^{r}, on the other hand, \underline{d} is the domain of syntactic term families, and the constants are reflected according to their types, as usual. In particular, reify\underline{d} is simply the identity.

The soundness result for TDPE then gives us that if ⊢_{Σ_{s},Σ_{d}} E : \underline{d} and Eval_{I_{s},I_{d}^{r}}(E) = ^{⌜}Ẽ^{⌝} then ⊢_{Σ_{d}}^{nf} Ẽ : \underline{d} and Eval_{I_{d}^{e}}(Ẽ) = Eval_{I_{s},I_{d}^{e}}(E). With a little more work we also obtain a similar statement for non-closed terms.

Note finally that normalizing a term of type \underline{d} a priori yields a simply-typed term over Σ_{d}, rather than an untyped one. In a static normal form, however, any occurrence of the constant \underline{ϕ} will be applied to a syntactic lambda-abstraction, and \underline{ψ} will be applied to two arguments. Thus, the output of the partial evaluator can always be directly expressed in terms of the underlined abstraction and application operators.

5.2 Gensym-like name generation

The term-family representation from Section 3.1 constructs terms in which the names of bound variables are derived from the number of enclosing lambdas; this convention is sometimes known as de Bruijn levels (not to be confused with de Bruijn indices). Although this is probably the simplest choice in a purely functional setting, there is nothing canonical about it. To more precisely capture the informal concept of newly-generated “fresh” variable names, we could instead take:

Λ̂ = N → (Λ × N)_{⊥}
{ \atop VAR} = λv.λi.val^{⊥} (VAR(v), i)
{ \atop LAM} = λ(t, ε).λi.let^{⊥} (l, i′) ⇐ εg_{i} (i + 1) in val^{⊥} (LAM (g_{i}, t, l), i′)
{ \atop APP} = λ(e_{1}, e_{2}).λi.let^{⊥} (l_{1}, i′) ⇐ e_{1} i in let^{⊥} (l_{2}, i′′) ⇐ e_{2} i′ in val^{⊥} (APP(l_{1}, l_{2}), i′′)

(with analogous extensions for constants and literals). This scheme generates terms in which all bound-variable names are distinct. Then, after changing the conditional meaning relation to read:

e @^{Δ} δ ≻_{τ}^{s} a ⟺

∀i ≥ ♯Δ. ei = ⊥ ∨ ∃E, i′ ≥ i. ei = val^{⊥} (^{⌜}E^{⌝}, i′) ∧ Δ ⊢_{Σ_{d}}^{s} E : τ ∧ [[E]]δ = a.

we can check that Lemma 3 still holds, and therefore all the remaining constructions and proofs go through without further modifications.

5.3 On-line type-directed partial evaluation

Although TDPE generally works on binding-time separated signatures, it is actually possible to give an on-line formulation, in which it is not necessary to explicitly annotate all base types and operations. Conceptually, we instead take B_{d}^{r}(b) = N → (B_{s}(b) + Λ)_{⊥}. (In practice, when Λ is a conveniently inspectable type, it suffices to take B_{d}^{r}(b) = Λ̂ and explicitly recognize Λ-values that represent literals.) The arithmetic operators then produce a static result if if both arguments are static, and dynamic otherwise, possibly coercing one argument in the process. A similar extension works for conditionals.

This scheme enables “opportunistic” simplifications, in cases where an operand is sometimes, but not always, statically known (or where a static analysis cannot prove that it is known). Note, however, that we must still annotate occurrences of fix as static or dynamic, or otherwise prevent fruitless infinite expansion of a recursive function. For example, it is often possible to explicitly identify a particular function parameter as the one controlling the recursion, and only unfold calls in which that argument is a literal [5].

Of course, the price of these potential improvements is that the amount of simplification is less predictable: the output will still be in long βη-normal form, but it is no longer evident from the original program which operations will be performed statically, and which ones must remain in the specialized program.

5.4 Call-by-value and effects

For practical applications, a call-by-value variant of TDPE is usually preferable, and indeed the technique was first presented in this setting [4]. Let us briefly sketch the necessary changes from the call-by-name case here.

To give a denotational semantics of an ML-like language, we consider an interpretation I to also explicitly include a monad for modeling effectful computations. We usually want to be able to use any monad in the evaluating interpretation; thus the notion of static equality must be safe for any dynamic effect. That is, instead of computing normal forms based on the strong βη-lambda-calculus, we now need a normalization-by-evaluation algorithm for Moggi’s computational lambdacalculus λ_{c} [15].

Fortunately, much as a single residualizing interpretation of dynamic type and term constants suffices to compute call-by-name static normal forms sound for any dynamic interpretation, it turns out that a single “maximally general” residualizing interpretation of effects can be used to compute call-by-value normal forms suitable for any dynamic monad.

A particularly natural such residualizing monad is that of continuations with answer type Λ̂, which can be straightforwardly related to any dynamic monad for the purpose of the logical relation in Section 4.2. Moreover, we can still construct the corresponding residualizing realization Φ^{r}, as long as our programming language contains Scheme-style first-class continuations and state [10]. Incidentally, this construction also allows disjoint-union types (sums) to be naturally added to the language. The details are still under investigation, however, and will be reported in a forthcoming paper.

6 Conclusions and Future Work

We have given an account of type-directed partial evaluation that separates the specification of the problem (computation of static normal forms) from its implementation (normalization by evaluation); in previous work these tended to be intertwined. We also presented a correctness proof for the implementation, using logical relations over a simple denotational model of the binding-time separated language. To keep the details manageable, we restricted our scope to a purely functional language; but both the algorithm and the proof techniques extend to call-by-value languages with effects as well.

Future work falls in two classes. First, there are a number of natural extensions to the framework and results in essentially the form they are presented here. In addition to the directions already mentioned in Section 5, one can also consider polyvariant specialization, run-time code generation, and other classical PE concepts in the context of TDPE.

Second, it would be interesting to investigate how TDPE relates to more general work on linguistic support for staged computation, especially recent developments based on modal logics [9, 16]. For example, it might be possible to generalize the notion of static normalization to such settings, and consider normalizationby-evaluation algorithms for type systems more expressive than simple types.

Acknowledgments

I want to thank Olivier Danvy for many deep and fruitful discussions about TDPE. I am also grateful to Daniel Damian, Bernd Grobauer, Zhe Yang, and the PPDP’99 reviewers for their careful reading and insightful comments on various drafts of this manuscript.

References

1. Ulrich Berger. Program extraction from normalization proofs. In M. Bezem and J. F. Groote, editors, Typed Lambda Calculi and Applications, number 664 in Lecture Notes in Computer Science, pages 91–106, Utrecht, The Netherlands, March 1993.

2. Ulrich Berger and Helmut Schwichtenberg. An inverse of the evaluation functional for typed λ-calculus. In Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science, pages 203–211, Amsterdam, The Netherlands, July 1991.

3. Thierry Coquand and Peter Dybjer. Intuitionistic model constructions and normalization proofs. Mathematical Structures in Computer Science, 7:75–94, 1997.

4. Olivier Danvy. Type-directed partial evaluation. In 23rd ACM Symposium on Principles of Programming Languages, pages 242–257, St. Petersburg Beach, Florida, January 1996.

5. Olivier Danvy. Online type-directed partial evaluation. In Masahiko Sato and Yoshihito Toyama, editors, Proceedings of the Third Fuji International Symposium on Functional and Logic Programming, pages 271–295, Kyoto, Japan, April 1998.

6. Olivier Danvy. Type-directed partial evaluation. Lecture Notes BRICS LN-98-3, Department of Computer Science, University of Aarhus, Aarhus, Denmark, December 1998. To appear in LNCS.

7. Olivier Danvy and Peter Dybjer, editors. Preliminary Proceedings of the APPSEM Workshop on Normalization by Evaluation, Chalmers, Sweeden, May 1998. BRICS Note NS-98-1.

8. Olivier Danvy and René Vestergaard. Semantics-based compiling: A case study in type-directed partial evaluation. In Eighth International Symposium on Programming Language Implementation and Logic Programming, number 1140 in Lecture Notes in Computer Science, pages 182–197, Aachen, Germany, September 1996.

9. Rowan Davies and Frank Pfenning. A modal analysis of staged computation. In 23rd ACM Symposium on Principles of Programming Languages, pages 258–270, St. Petersburg Beach, Florida, January 1996.

10. Andrzej Filinski. Representing monads. In Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 446–457, Portland, Oregon, January 1994.

11. William L. Harrison and Samuel N. Kamin. Modular compilers based on monad transformers. In Proceedings of the IEEE International Conference on Computer Languages, pages 122–131, Chicago, Illinois, May 1998. IEEE Computer Society.

12. Simon Helsen and Peter Thiemann. Two flavors of offline partial evaluation. In J. Hsiang and A. Ohori, editors, Advances in Computing Science – ASIAN’98, number 1538 in Lecture Notes in Computer Science, pages 188–205, Manilla, The Philippines, December 1998.

13. Carsten Kehler Holst and John Launchbury. Handwriting cogen to avoid problems with static typing. In Draft Proceedings, Fourth Annual Glasgow Workshop on Functional Programming, pages 210–218, Skye, Scotland, 1991.

14. Neil D. Jones, Carsten K. Gomard, and Peter Sestoft. Partial Evaluation and Automatic Program Generation. Prentice Hall International Series in Computer Science. Prentice-Hall, 1993.

15. Eugenio Moggi. Computational lambda-calculus and monads. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science, pages 14–23, Pacific Grove, California, June 1989. IEEE.

16. Eugenio Moggi, Walid Taha, Zine El-Abidine Benaissa, and Tim Sheard. An idealized MetaML: Simpler and more expressive. In 8th European Symposium on Programming Languages and Systems, number 1576 in Lecture Notes in Computer Science, pages 193–207, Amsterdam, The Netherlands, March 1999.

17. Gordon D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5(3):223–255, December 1977.

18. Zhe Yang. Encoding types in ML-like languages. In International Conference on Functional Programming, pages 289–300, Baltimore, Maryland, September 1998.