BRICS Basic Research in Computer Science

B R ICS R S -02-52 O. Dan vy: A N ew On e-P ass T ran sf ormation in to Mon a d ic N ormal F orm

BRICS

Basic Research in Computer Science

A New One-Pass Transformation into Monadic Normal Form

Olivier Danvy

BRICS Report Series RS-02-52

Copyright c 2002, Olivier Danvy.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications.

Copies may be obtained by contacting:

BRICS

Department of Computer Science University of Aarhus

Ny Munkegade, building 540 DK–8000 Aarhus C

Denmark

Telephone: +45 8942 3360 Telefax: +45 8942 3255 Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk ftp://ftp.brics.dk

This document in subdirectory RS/02/52/

A New One-Pass Transformation into Monadic Normal Form ^∗

Olivier Danvy BRICS

Department of Computer Science University of Aarhus

December 2002

Abstract

We present a translation from the call-by-valueλ-calculus to monadic normal forms that includes short-cut boolean evaluation. The translation is higher-order, operates in one pass, duplicates no code, generates no chains of thunks, and is properly tail recursive. It makes a crucial use of symbolic computation at translation time.

∗To appear in the proceedings of CC 2003.

†Basic Research in Computer Science (www.brics.dk), funded by the Danish National Research Foundation.

‡Ny Munkegade, Building 540, DK-8000 Aarhus C, Denmark E-mail:danvy@brics.dk

Contents

1 Introduction 3

2 A Standard, Two-Pass Translation 5

3 A One-Pass Translation 5

4 Two Examples 9

4.1 No chains of thunks . . . 9 4.2 Short-cut boolean evaluation . . . 9

5 Assessment 9

6 Related Work, Conclusion, and Future Work 10

A Two-Level Programming in ML 10

1 Introduction

Program transformation and code generators offer typical situations where sym- bolic computation makes it possible to merge several passes into one. The CPS transformation is a canonical example: it transforms a term in direct style into one in continuation-passing style (CPS) [39, 43]. It appears in several Scheme compilers, including the first one [30, 33, 42], where it is used in two passes:

one for the transformation proper and one for the simplifications entailed by the transformation (the so-called “administrative redexes”). One-pass versions have been developed that perform administrative reductions at transformation time [2, 15, 48]. They form one of the first, if not the first, instances of higher- order and natively executable two-level specifications.

The notion of binding times was discovered early by Jones and Muchnick [27]

in the context of programming languages. Later it proved instrumental for partial evaluation [28], for program analysis [37], and for code generation [50]. It was then soon noticed that two-level specifications (i.e., ‘staged’ [29], or ‘binding- time separated’ [35], or again ‘binding-time analyzed’ [25] specifications) were directly expressible in languages such as Lisp and Scheme that offer quasiquote and unquote—a metalinguistic capability that has since been rediscovered in

‘C [19], cast in a typed setting in MetaML [45], and connected both to modal logic [18] and to temporal logic [17]. In Lisp, quasiquote and unquote are used chiefly to write macros [5], an early example of symbolic computation during code generation [32]. In partial evaluation [10, 26], two-level specifications are called ‘generating extensions’. Nesting quasiquote and unquote yields macros that generate macros and multi-level generating extensions.

The goal of this article is to present a one-pass transformer into monadic normal forms [23, 36] that performs short-cut boolean evaluation, duplicates no code, generates no chains of thunks, and is properly tail recursive. We consider the following source language:

Λ^E3e ::= ` | x | λx.e | e e | ifbtheneelsee Λ^B 3b ::= e | b∧b | b∨b | ¬b | ifbthenbelseb

We translate programs in this source language into programs in the following target language:

Λ^C_ml 3c ::= returnv |

letx=v vinc | v v | ifvthencelsec | letx=λ().cinc | x() Λ^V_ml 3v ::= ` | x | λx.c

The source language is that of the call-by-value λ-calculus with literals, con- ditional expressions, and computational effects. The target language is that of monadic normal forms (sometimes called A-normal forms [21]), with a syn- tactic separation between computations (c, the serious expressions) and values

(v, the trivial expressions), as traditional since Reynolds and Moggi [36, 41].

The return production is the unit and the first let production is the bind of monadic style [47]. Computations are carried out by applications, which can either be named with a let expression or occur in tail position. Conditional expressions exclusively occur in tail position. The last two productions specify the declaration and activation of thunks, which are used to ensure that no code is duplicated.

For example, a source term such as

λx.g₀(h₀(if(g₁(h₁x))∨xtheng₂(h₂x)elsex))

is translated into the following target term (automatically pretty printed in Standard ML for clarity), in one pass.

return (fn x => let val k0 = fn w1 => let val w2 = h0 w1 in g0 w2

end

val t5 = fn () => let val w3 = h2 x val w4 = g2 w3 in k0 w4

end val w6 = h1 x

val w7 = g1 w6 in if w7

then t5 () else if x

then t5 () else k0 x end)

In this target term, the source contextg₀(h₀[·]) is translated into the function k0, where the outside call occurs tail recursively. Because of the disjunction in the test, a thunk t5is created for the then branch. In this thunk, the outside call occurs tail recursively. The composition ofg₁ andh₁ is sequentialized and its result is tested. If it holds true, t5 is activated; otherwise, the second half of the disjunction is tested. If it holds true,t5 is activated (the code for t5is shared). Otherwise, the value ofxis passed to the (sequentialized) composition ofg₀andh₀. Free variables (i.e.,g₀,h₀,g₁,h₁,g₂, andh₂) have been translated to themselves (i.e.,g0,h0,g1, h1,g2, andh2, respectively).

Monadic normal forms offer the main advantages of CPS (i.e., all intermedi- ate results are named and their computation is sequentialized),¹and they have been used in compilers for functional languages [6,7,21–23,38,40,46]. Therefore, a one-pass transformation into monadic normal form with short-cut boolean evaluation could well be of practical use (i.e., outside academia).

The rest of this article is organized as follows. We present a standard, two- pass translation from the source language to the target language (Section 2),

1The jury is still out about the other advantages of CPS [40].

and then its one-pass counterpart (Section 3). We then illustrate it (Section 4), assess it (Section 5), and then review related work and conclude (Section 6).

2 A Standard, Two-Pass Translation

The first part of the translation is simple enough: it is the standard encoding of the call-by-value λ-calculus into the computational metalanguage, straight- forwardly extended to handle conditional expressions.

Ev[[`]] = return` Ev[[x]] = returnx E_v[[λx.e]] = returnλx.E_v[[e]]

Ev[[e₀e₁]] = letw₀=Ev[[e₀]]in letw₁=Ev[[e₁]]inw₀w₁ E_v[[ifbthene₁elsee₀]] = ifB_v[[b]]thenE_v[[e₁]]elseE_v[[e₀]]

B_v[[e]] = E_v[[e]]

Bv[[b₁∧b₂]] = ifBv[[b₁]]thenBv[[b₂]]elsefalse B_v[[b₁∨b₂]] = ifB_v[[b₁]]thentrueelseB_v[[b₂]]

Bv[[¬b]] = ifBv[[b]]thenfalseelsetrue B_v[[ifb₂thenb₁elseb₀]] = ifB_v[[b₂]]thenB_v[[b₁]]elseB_v[[b₀]]

The second pass of the translation consists in performing monadic simplifi- cations [24] and in unnesting conditional expressions until the simplified term belongs to Λ^C_ml.

3 A One-Pass Translation

In this section, we build on the full one-pass transformation into monadic normal form for the call-by-valueλ-calculus:

E : Λ^E →Λ^C_ml E[[`]] = return` E[[x]] = returnx E[[λx.e]] = returnλx.E[[e]]

E[[e0e₁]] = Ec[[e₀]]λv₀.Ec[[e₁]]λv₁.v₀@v₁ E_c : Λ^E →(Λ^V_ml →Λ^C_ml)→Λ^C_ml Ec[[`]]κ = κ@`

Ec[[x]]κ = κ@x E_c[[λx.e]]κ = κ@λx.E[[e]]

Ec[[e₀e₁]]κ = Ec[[e₀]]λv₀.Ec[[e₁]]λv₁.letw=v₀@v₁inκ@w

The functionEis applied to subterms occurring in tail position, and the function Ec to the other subterms; it is indexed with a functional accumulatorκ.² This transformation is higher-order (witness the type ofEc) and it is also two level:

the underlined terms are hygienic syntax constructors and the overlined terms are reduced at transformation time (@ denotes infix application). We show in appendix how to program it in ML. This transformation is similar to a higher- order one-pass CPS transformation, which can be transformationally derived from a two-pass specification [16].

The question now is to generalize this one-pass transformation to the full Λ^E and Λ^B from Section 1. Our insight is to index the translation of each boolean expression with the translation of the corresponding consequent and alternative. Each of them can be the name of a thunk, which we can use non- linearly, or a thunk, which we should only use linearly since we want to avoid code duplication. Enumerating, we define four translation functions for boolean expressions:

Bcc : Λ^B →(1→Λ^C_ml)×(1→Λ^C_ml)→Λ^C_ml B_vv : Λ^B →Λ^V_ml×Λ^V_ml →Λ^C_ml

Bcv : Λ^B →(1→Λ^C_ml)×Λ^V_ml →Λ^C_ml B_vc : Λ^B →Λ^V_ml×(1→Λ^C_ml)→Λ^C_ml

The problem then reduces to following the structure of the boolean expressions and introducing residual let expressions to name computations if their result needs to be used more than once.

B_cc : Λ^B→(1→Λ^C_ml)×(1→Λ^C_ml)→Λ^C_ml Bcc[[b₁∧b₂]]hκ₁, κ₀i = lett₀=λ().κ₀@ ()

inB_cv[[b₁]]hλ().B_cv[[b₂]]hκ₁, t₀i, t₀i B_cc[[b₁∨b₂]]hκ₁, κ₀i = lett₁=λ().κ₁@ ()

inBvc[[b₁]]ht₁, λ().Bvc[[b₂]]ht₁, κ₀ii Bcc[[¬b]]hκ₁, κ₀i = Bcc[[b]]hκ₀, κ₁i

Bcc[[ifb₂thenb₁elseb₀]]hκ₁, κ₀i = lett₁=λ().κ₁@ () in lett₀=λ().κ₀@ ()

inB_cc[[b₂]]hλ().B_vv[[b₁]]ht₁, t₀i, λ().B_vv[[b₀]]ht₁, t₀ii

For example, let us consider B_cc[[b₁∧b₂]]hκ₁, κ₀i, i.e., the translation of a conjunction in the presence of two thunksκ₁ andκ₀. The activation ofκ₁ and κ₀ will yield the translation of the consequent and of the alternative of this

2We refrain from referring toκas a continuation since it is not applied tail recursively.

conjunction. Naively, we could want to define the translation as follows:

Bcc[[b₁]]hλ().Bcc[[b₂]]hκ₁, κ₀i, κ₀i

Doing so, however, would duplicate κ₀, i.e., the translation of the alternative of the conjunction. Therefore we name its result with a let. The rest of the translation follows the same spirit.

Bvv : Λ^B→Λ^V_ml×Λ^V_ml →Λ^C_ml Bvv[[b₁∧b₂]]hv₁, v₀i = Bcv[[b₁]]hλ().Bvv[[b₂]]hv₁, v₀i, v₀i Bvv[[b₁∨b₂]]hv₁, v₀i = Bvc[[b₁]]hv₁, λ().Bvv[[b₂]]hv₁, v₀ii

B_vv[[¬b]]hv₁, v₀i = B_vv[[b]]hv₀, v₁i

Bvv[[ifb₂thenb₁elseb₀]]hv₁, v₀i = Bcc[[b₂]]hλ().Bvv[[b₁]]hv₁, v₀i, λ().Bvv[[b₀]]hv₁, v₀ii Bcv : Λ^B→(1→Λ^C_ml)×Λ^V_ml →Λ^C_ml Bcv[[b₁∧b₂]]hκ₁, v₀i = Bcv[[b₁]]hλ().Bcv[[b₂]]hκ₁, v₀i, v₀i Bcv[[b₁∨b₂]]hκ₁, v₀i = lett₁=λ().κ₁@ ()

inB_vc[[b₁]]ht₁, λ().B_vv[[b₂]]ht₁, v₀ii Bcv[[¬b]]hκ₁, v₀i = Bvc[[b]]hv₀, κ₁i

B_cv[[ifb₂thenb₁elseb₀]]hκ₁, v₀i = lett₁=λ().κ₁@ ()

inBcc[[b₂]]hλ().Bvv[[b₁]]ht₁, v₀i, λ().Bvv[[b₀]]ht₁, v₀ii Bvc : Λ^B→Λ^V_ml×(1→Λ^C_ml)→Λ^C_ml B_vc[[b₁∧b₂]]hv₁, κ₀i = lett₀=λ().κ₀@ ()

inBcv[[b₁]]hλ().Bvv[[b₂]]hv₁, t₀i, t₀i Bvc[[b₁∨b₂]]hv₁, κ₀i = Bvc[[b₁]]hv₁, λ().Bvc[[b₂]]hv₁, κ₀ii

Bvc[[¬b]]hv₁, κ₀i = Bcv[[b]]hκ₀, v₁i Bvc[[ifb₂thenb₁elseb₀]]hv₁, κ₀i = lett₀=λ().κ₀@ ()

inB_cc[[b₂]]hλ().B_vv[[b₁]]hv₁, t₀i, λ().Bvv[[b₀]]hv₁, t₀ii

As for the connection between translating a boolean expression and translat- ing an expression, we make it using a functional accumulator that will generate a conditional expression when it is applied.

Bcc[[e]]hκ₁, κ₀i = Ec[[e]]λv.ifvthenκ₁@ ()elseκ₀@ () B_vv[[e]]hv₁, v₀i = E_c[[e]]λv.ifvthenv₁@ ()elsev₀@ () B_cv[[e]]hκ₁, v₀i = E_c[[e]]λv.ifvthenκ₁@ ()elsev₀@ () Bvc[[e]]hv₁, κ₀i = Ec[[e]]λv.ifvthenv₁@ ()elseκ₀@ ()

Finally we connect translating an expression and translating a boolean ex- pression as follows.

E[[ifbthene₁elsee₀]] = Bcc[[b]]hλ().E[[e₁]], λ().E[[e₀]]i Ec[[ifbthene₁elsee₀]]κ = letk=λw.κ@w

inBcc[[b]]hλ().Ev[[e₁]]k, λ().Ev[[e₀]]ki E_v : Λ^E →Λ^V_ml →Λ^C_ml

Ev[[`]]k = k@` E_v[[x]]k = k@x Ev[[λx.e]]k = k@λx.E[[e]]

Ev[[e₀e₁]]k = Ec[[e₀]]λv₀.Ec[[e₁]]λv₁.letw=v₀@v₁ink@w Ev[[ifbthene₁elsee₀]]k = Bcc[[b]]hλ().Ev[[e₁]]k, λ().Ev[[e₀]]ki

In the second equation, a let expression is inserted to name the context (and to avoid its duplication). E_v is there to avoid generating chains of thunks when translating nested conditional expressions.

The result can be directly coded in ML (see appendix): the source and target languages are implemented as data types and the translation as a function. A side benefit of using ML is that its type inferencer acts as a theorem prover to tell us that the translation maps terms from the source language into terms in the target language (a bit more reasoning, however, is necessary to show that the translation generates no chains of thunks). Finally, since the translation is specified compositionally, it does operate in one pass.

4 Two Examples

4.1 No chains of thunks

The term λx.g(h(ifathen ifb₂thenb₁elseb₀elsex)) is translated into the fol- lowing target term in one pass.

return (fn x => let val k0 = fn v1 => let val v2 = h v1 in g v2

end in if a

then if b2 then k0 b1 else k0 b0 else k0 x end)

Each conditional branch directly callsk0. 4.2 Short-cut boolean evaluation

The termλx.ifa₁∧a₂∧a₃∧a₄thenxelseg(h x) is translated into the follow- ing target term in one pass.

return (fn x => let val f1 = fn () => let val v0 = h x in g v0

end in if a1

then if a2 then if a3

then if a4

then return x else f1 () else f1 () else f1 () else f1 () end)

All the else branches directly callf1.

5 Assessment

A similar development yields, mutatis mutandis, a CPS transformation that is higher-order, operates in one pass, duplicates no code, generates no chain of thunks, and is properly tail recursive.

The author has implemented both transformations in his academic Scheme compiler. Their net effect is to fuse two compiler passes into one and to avoid, in effect, an entire copy of the source program. In particular, an escape analysis of the transformations themselves shows that all of their higher-order functions are stack-allocatable [4]. The transformations therefore have a minimal footprint in

that they only allocate heap space to construct their result, making them well suited in a JIT situation.

6 Related Work, Conclusion, and Future Work

We have presented a two-level program transformation that encodes call-by- valueλ-terms into monadic normal form and achieves short-cut boolean evalua- tion. The transformation operates in one pass in that it directly constructs the normal form without intermediate representations that need further processing.

As usual with two-level specifications, erasing all overlines and underlines yields something meaningful—here an interpreter for the call-by-valueλ-calculus in the monadic metalanguage.

The program transformation can be easily adapted to other evaluation or- ders.

Short-cut evaluation is a standard topic in compiling [1,9,34]. The author is not aware of any treatment of it in one-pass CPS transformations or in one-pass transformations into monadic normal form.

Our use of higher-order functions and of an underlying evaluator to fuse a transformation and a form of normalization is strongly reminiscent of the notion ofnormalization by evaluation[8,11,13,20]. And indeed the author is convinced that the present one-pass transformation could be specified as a formal instance of normalization by evaluation—a future work.

Monadic normal forms and CPS terms are in one-to-one correspondence [12], and Kelsey and Appel have noticed the correspondence between continuation- passing style and static single assignment form (SSA) [3, 31]. Therefore, the one-pass transformation with short-cut boolean evaluation should apply directly to the SSA transformation [49]—another future work.

Acknowledgments: Thanks are due to Mads Sig Ager, Jacques Carette, Samuel Lindley, and the anonymous reviewers for comments.

This work is supported by the ESPRIT Working Group APPSEM II (http://www.tcs.informatik.uni-muenchen.de/~mhofmann/appsem2/).

A Two-Level Programming in ML

We briefly outline how to program the one-pass translation of Section 2 [14].

First, we assume a type for identifiers as well as a module generating fresh identifiers in the target abstract syntax:

type ide = string signature GENSYM = sig

val init : unit -> unit val new : string -> ide end

Given this type, the source and the target abstract syntax (without condi- tional expressions) are defined with two data types:

structure Source = struct

datatype e = VAR of ide

| LAM of ide * e

| APP of e * e end

structure Target = struct

datatype e = RETURN of t

| TAIL_APP of t * t

| LET_APP of ide * (t * t) * e and t = VAR of ide

| LAM of ide * e end

Given a structureGensym : GENSYM, the two translation functionsE andE_c are recursively defined as two ML functions trans0 andtrans1. In particular, trans1 is uncurried and higher order. For readability of the output, the main translation function trans initializes the generator of fresh identifiers before callingtrans0:

(* trans0 : Source.e -> Target.e *)

(* trans1 : Source.e * (Target.t -> Target.e) -> Target.e *) fun trans0 (Source.VAR x)

= Target.RETURN (Target.VAR x)

| trans0 (Source.LAM (x, e))

= Target.RETURN (Target.LAM (x, trans0 e))

| trans0 (Source.APP (e0, e1))

= trans1 (e0,

fn v0 => trans1 (e1,

fn v1 => Target.TAIL_APP (v0, v1))) and trans1 (Source.VAR x, k)

= k (Target.VAR x)

| trans1 (Source.LAM (x, e), k)

= k (Target.LAM (x, trans0 e))

| trans1 (Source.APP (e0, e1), k)

= trans1 (e0,

fn v0 => trans1 (e1,

fn v1 => let val v = Gensym.new "v"

in Target.LET_APP (v,

(v0, v1),

k (Target.VAR v)) end))

(* trans : Source.e -> Target.e *) fun trans e

= (Gensym.init (); trans0 e)

References

[1] Alfred V. Aho, Ravi Sethi, and Jeffrey D. Ullman. Compilers: Principles, Techniques and Tools. World Student Series. Addison-Wesley, Reading, Massachusetts, 1986.

[2] Andrew W. Appel. Compiling with Continuations. Cambridge University Press, New York, 1992.

[3] Andrew W. Appel. SSA is functional programming. ACM SIGPLAN No- tices, 33(4):17–20, April 1998.

[4] Anindya Banerjee and David A. Schmidt. Stackability in the typed call- by-value lambda calculus.Science of Computer Programming, 31(1):47–73, 1998.

[5] Alan Bawden. Quasiquotation in Lisp. In Olivier Danvy, editor,Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Semantics- Based Program Manipulation, Technical report BRICS-NS-99-1, University of Aarhus, pages 4–12, San Antonio, Texas, January 1999. Available online at http://www.brics.dk/~pepm99/programme.html.

[6] Nick Benton and Andrew Kennedy. Monads, effects, and transformations.

InThird International Workshop on Higher-Order Operational Techniques in Semantics, volume 26 ofElectronic Notes in Theoretical Computer Sci- ence, pages 19–31, Paris, France, September 1999.

[7] Nick Benton, Andrew Kennedy, and George Russell. Compiling Standard ML to Java byte-codes. In Paul Hudak and Christian Queinnec, editors, Proceedings of the 1998 ACM SIGPLAN International Conference on Func- tional Programming, pages 129–140, Baltimore, Maryland, September 1998.

ACM Press.

[8] Ulrich Berger, Matthias Eberl, and Helmut Schwichtenberg. Normalization by evaluation. In Bernhard M¨oller and John V. Tucker, editors,Prospects for hardware foundations (NADA), number 1546 in Lecture Notes in Com- puter Science, pages 117–137. Springer-Verlag, 1998.

[9] Keith Clarke. One-pass code generation using continuations. Software—

Practice and Experience, 19(12):1175–1192, 1989.

[10] Charles Consel and Olivier Danvy. Tutorial notes on partial evalua- tion. In Susan L. Graham, editor, Proceedings of the Twentieth Annual ACM Symposium on Principles of Programming Languages, pages 493–501, Charleston, South Carolina, January 1993. ACM Press.

[11] Thierry Coquand and Peter Dybjer. Intuitionistic model constructions and normalization proofs.Mathematical Structures in Computer Science, 7:75–

94, 1997.

[12] Olivier Danvy. Back to direct style. Science of Computer Programming, 22(3):183–195, 1994.

[13] Olivier Danvy. Type-directed partial evaluation. In John Hatcliff, Tor- ben Æ. Mogensen, and Peter Thiemann, editors,Partial Evaluation – Prac- tice and Theory; Proceedings of the 1998 DIKU Summer School, number 1706 in Lecture Notes in Computer Science, pages 367–411, Copenhagen, Denmark, July 1998. Springer-Verlag.

[14] Olivier Danvy. Programming techniques for partial evaluation. In Friedrich L. Bauer and Ralf Steinbr¨uggen, editors, Foundations of Secure Computation, NATO Science series, pages 287–318. IOS Press Ohmsha, 2000.

[15] Olivier Danvy and Andrzej Filinski. Abstracting control. In Mitchell Wand, editor, Proceedings of the 1990 ACM Conference on Lisp and Functional Programming, pages 151–160, Nice, France, June 1990. ACM Press.

[16] Olivier Danvy and Lasse R. Nielsen. A first-order one-pass CPS transforma- tion. In Mogens Nielsen and Uffe Engberg, editors,Foundations of Software Science and Computation Structures, 5th International Conference, FOS- SACS 2002, number 2303 in Lecture Notes in Computer Science, pages 98–113, Grenoble, France, April 2002. Springer-Verlag. Extended version available as the technical report BRICS RS-01-49. To appear in TCS.

[17] Rowan Davies. A temporal-logic approach to binding-time analysis. In Edmund M. Clarke, editor,Proceedings of the Eleventh Annual IEEE Sym- posium on Logic in Computer Science, pages 184–195, New Brunswick, New Jersey, July 1996. IEEE Computer Society Press.

[18] Rowan Davies and Frank Pfenning. A modal analysis of staged computa- tion. In Steele Jr. [44], pages 258–283.

[19] Dawson R. Engler, Wilson C. Hsieh, and M. Frans Kaashoe. ‘C: A language for high-level, efficient, and machine-independent dynamic code generation.

In Steele Jr. [44], pages 131–144.

[20] Andrzej Filinski. Normalization by evaluation for the computational lambda-calculus. In Samson Abramsky, editor,Typed Lambda Calculi and Applications, 5th International Conference, TLCA 2001, number 2044 in Lecture Notes in Computer Science, pages 151–165, Krak´ow, Poland, May 2001. Springer-Verlag.

[21] Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. The essence of compiling with continuations. In David W. Wall, editor, Pro- ceedings of the ACM SIGPLAN’93 Conference on Programming Languages Design and Implementation, SIGPLAN Notices, Vol. 28, No 6, pages 237–

247, Albuquerque, New Mexico, June 1993. ACM Press.

[22] Matthew Fluet and Stephen Weeks. Contification using dominators. In Xavier Leroy, editor, Proceedings of the 2001 ACM SIGPLAN Interna- tional Conference on Functional Programming, SIGPLAN Notices, Vol. 36, No. 10, pages 2–13, Firenze, Italy, September 2001. ACM Press.

[23] John Hatcliff and Olivier Danvy. A generic account of continuation-passing styles. In Hans-J. Boehm, editor, Proceedings of the Twenty-First Annual ACM Symposium on Principles of Programming Languages, pages 458–471, Portland, Oregon, January 1994. ACM Press.

[24] John Hatcliff and Olivier Danvy. A computational formalization for partial evaluation. Mathematical Structures in Computer Science, pages 507–541, 1997. Extended version available as the technical report BRICS RS-96-34.

[25] Neil D. Jones. Tutorial on binding time analysis. In Paul Hudak and Neil D. Jones, editors, Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, SIGPLAN Notices, Vol. 26, No 9, New Haven, Connecticut, June 1991. ACM Press.

[26] Neil D. Jones, Carsten K. Gomard, and Peter Sestoft. Partial Evalua- tion and Automatic Program Generation. Prentice-Hall International, Lon- don, UK, 1993. Available online athttp://www.dina.kvl.dk/~sestoft/

pebook/.

[27] Neil D. Jones and Steven S. Muchnick. Some thoughts towards the design of an ideal language. In Susan L. Graham, editor,Proceedings of the Third Annual ACM Symposium on Principles of Programming Languages, pages 77–94. ACM Press, January 1976.

[28] Neil D. Jones, Peter Sestoft, and Harald Søndergaard. MIX: A self- applicable partial evaluator for experiments in compiler generation. Lisp and Symbolic Computation, 2(1):9–50, 1989.

[29] Ulrik Jørring and William L. Scherlis. Compilers and staging transforma- tions. In Mark Scott Johnson and Ravi Sethi, editors, Proceedings of the Thirteenth Annual ACM Symposium on Principles of Programming Lan- guages, pages 86–96, St. Petersburg, Florida, January 1986. ACM Press.

[30] Richard A. Kelsey. Compilation by Program Transformation. PhD thesis, Computer Science Department, Yale University, New Haven, Connecticut, May 1989. Research Report 702.

[31] Richard A. Kelsey. A correspondence between continuation passing style and static single assignment form. In Michael Ernst, editor, ACM SIG- PLAN Workshop on Intermediate Representations, SIGPLAN Notices, Vol. 30, No 3, pages 13–22, San Francisco, California, January 1995. ACM Press.

[32] Oleg Kiselyov. Macros that compose: Systematic macro programming. In Don Batory, Charles Consel, and Walid Taha, editors, Proceedings of the 2002 ACM SIGPLAN/SIGSOFT Conference on Generative Programming and Component Engineering, number 2487 in Lecture Notes in Computer Science, pages 202–217, Pittsburgh, Pennsylvania, October 2002. Springer- Verlag.

[33] David A. Kranz.ORBIT: An Optimizing Compiler for Scheme. PhD thesis, Computer Science Department, Yale University, New Haven, Connecticut, February 1988. Research Report 632.

[34] George Logothetis and Prateek Mishra. Compiling short-circuit boolean expressions in one pass. Software—Practice and Experience, 11:1197–1214, 1981.

[35] Torben Æ. Mogensen. Separating binding times in language specifications.

In Joseph E. Stoy, editor,Proceedings of the Fourth International Confer- ence on Functional Programming and Computer Architecture, pages 14–25, London, England, September 1989. ACM Press.

[36] Eugenio Moggi. Notions of computation and monads. Information and Computation, 93:55–92, 1991.

[37] Flemming Nielson and Hanne Riis Nielson. Two-Level Functional Lan- guages, volume 34 ofCambridge Tracts in Theoretical Computer Science.

Cambridge University Press, 1992.

[38] Dino P. Oliva and Andrew P. Tolmach. From ML to Ada: strongly-typed language interoperability via source translation.Journal of Functional Pro- gramming, 8(4):367–412, 1998.

[39] Gordon D. Plotkin. Call-by-name, call-by-value and theλ-calculus. Theo- retical Computer Science, 1:125–159, 1975.

[40] John Reppy. Optimizing nested loops using local CPS conversion.Higher- Order and Symbolic Computation, 15(2/3), 2002. To appear.

[41] John C. Reynolds. Definitional interpreters for higher-order programming languages. Higher-Order and Symbolic Computation, 11(4):363–397, 1998.

Reprinted from the proceedings of the 25th ACM National Conference (1972).

[42] Guy L. Steele Jr. Lambda, the ultimate declarative. AI Memo 379, Artificial Intelligence Laboratory, Massachusetts Institute of Technology, Cambridge, Massachusetts, November 1976.

[43] Guy L. Steele Jr. Rabbit: A compiler for Scheme. Master’s thesis, Artificial Intelligence Laboratory, Massachusetts Institute of Technology, Cambridge, Massachusetts, May 1978. Technical report AI-TR-474.

[44] Guy L. Steele Jr., editor. Proceedings of the Twenty-Third Annual ACM Symposium on Principles of Programming Languages, St. Petersburg Beach, Florida, January 1996. ACM Press.

[45] Walid Taha.Multi-Stage Programming: Its Theory and Applications. PhD thesis, Oregon Graduate Institute of Science and Technology, Portland, Oregon, 1999. CSE-99-TH-002.

[46] David Tarditi, Greg Morrisett, Perry Cheng, and Chris Stone. TIL: a type-directed optimizing compiler for ML. In Proceedings of the ACM SIGPLAN’96 Conference on Programming Languages Design and Imple- mentation, SIGPLAN Notices, Vol. 31, No 5, pages 181–192. ACM Press, June 1996.

[47] Philip Wadler. The essence of functional programming (invited talk). In Andrew W. Appel, editor,Proceedings of the Nineteenth Annual ACM Sym- posium on Principles of Programming Languages, pages 1–14, Albuquerque, New Mexico, January 1992. ACM Press.

[48] Mitchell Wand. Correctness of procedure representations in higher-order assembly language. In Stephen Brookes, Michael Main, Austin Melton, Michael Mislove, and David Schmidt, editors, Mathematical Foundations of Programming Semantics, number 598 in Lecture Notes in Computer Science, pages 294–311, Pittsburgh, Pennsylvania, March 1991. Springer- Verlag. 7th International Conference.

[49] Mark N. Wegman and F. Ken Zadeck. Constant propagation with condi- tional branches. ACM Transactions on Programming Languages and Sys- tems, 3(2):181–210, 1991.

[50] Zhe Yang. Language Support for Program Generation: Reasoning, Imple- mentation, and Applications. PhD thesis, Computer Science Department, New York University, New York, New York, August 2001.

Recent BRICS Report Series Publications

RS-02-52 Olivier Danvy. A New One-Pass Transformation into Monadic Normal Form. December 2002. 16 pp. To appear in Hedin, editor, Compiler Construction, 12th International Conference, CC ’03 Proceedings, LNCS, 2003.

RS-02-51 Gerth Stølting Brodal, Rolf Fagerberg, Anna ¨ Ostlin, Christian N. S. Pedersen, and S. Srinivasa Rao. Computing Refined Bune- man Trees in Cubic Time. December 2002. 14 pp.

RS-02-50 Kristoffer Arnsfelt Hansen, Peter Bro Miltersen, and V. Vinay.

Circuits on Cylinders. December 2002. 16 pp.

RS-02-49 Mikkel Nygaard and Glynn Winskel. HOPLA—A Higher- Order Process Language. December 2002. 18 pp. Appears in Brim, Janˇcar, Kˇret´ınsk´y and Anton´ın, editors, Concurrency Theory: 13th International Conference, CONCUR ’02 Proceed- ings, LNCS 2421, 2002, pages 434–448.

RS-02-48 Mikkel Nygaard and Glynn Winskel. Linearity in Process Lan- guages. December 2002. 27 pp. Appears in Plotkin, editor, Seventeenth Annual IEEE Symposium on Logic in Computer Science, LICS ’02 Proceedings, 2002, pages 433–446.

RS-02-47 Zolt´an ´ Esik. Extended Temporal Logic on Finite Words and Wreath Product of Monoids with Distinguished Generators. De- cember 2002. 16 pp. To appear in 6th International Conference, Developments in Language Theory, DLT ’02 Revised Papers, LNCS, 2002.

RS-02-46 Zolt´an ´ Esik and Hans Leiß. Greibach Normal Form in Alge- braically Complete Semirings. December 2002. 43 pp. An ex- tended abstract appears in Bradfield, editor, European Associ- ation for Computer Science Logic: 16th International Workshop, CSL ’02 Proceedings, LNCS 2471, 2002, pages 135–150.

RS-02-45 Jesper Makholm Byskov. Chromatic Number in Time O (2 . 4023

) Using Maximal Independent Sets. December 2002.

6 pp.