BRICS RS-00-35 Danvy & Nielsen: CPS Transformation of Beta-Redexes BRICS

Basic Research in Computer Science

CPS Transformation of Beta-Redexes

Olivier Danvy Lasse R. Nielsen BRICS Report Series RS-00-35 ISSN 0909-0878 December 2000 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2000, Olivier Danvy & Lasse R. Nielsen.

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/00/35/

CPS Transformation of Beta-Redexes ^{∗}

Olivier Danvy and Lasse R. Nielsen

BRICS ^{†}

Department of Computer Science University of Aarhus ^{‡}

December 21, 2000

Abstract

The extra compaction of Sabry and Felleisen’s transformation is due to making continuations occur first in CPS terms and classifying more redexes as administrative. We show that the extra compaction is actually independent of the relative positions of values and continuations and furthermore that it is solely due to a context-sensitive transformation of beta-redexes. We stage the more compact CPS transformation into a firstorder uncurrying phase and a context-insensitive CPS transformation. We also define a context-insensitive CPS transformation that is just as compact. This CPS transformation operates in one pass and is dependently typed.

Keywords: Continuation-passing style (CPS), Plotkin, Fischer, one-pass CPS transformation, two-level λ-calculus, generalized reduction.

∗To appear in the proceedings of the Third ACM SIGPLAN Workshop on Continuations (CW’01), January 16, 2001, London, UK.

† Basic Research in Computer Science (http://www.brics.dk/), Centre of the Danish National Research Foundation.

‡ Ny Munkegade, Building 540, DK-8000 Aarhus C, Denmark.

E-mail: {danvy,lrn}@brics.dk

Contents

1 Introduction 3 1.1 Continuation-passing style (CPS) . . . . . . . . . . . . . . . . . . 3 1.2 The CPS transformation . . . . . . . . . . . . . . . . . . . . . . . 3 1.3 Sabry and Felleisen’s optimization . . . . . . . . . . . . . . . . . 3 1.4 This article . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4

2 Administrative reductions in the CPS transformation 4 2.1 Context-insensitive administrative reductions . . . . . . . . . . . 4 2.2 Context-sensitive administrative reductions . . . . . . . . . . . . 5 2.3 CPS transformation of let expressions . . . . . . . . . . . . . . . 6 2.4 CPS transformation of embedded β-redexes . . . . . . . . . . . . 6 2.5 Summary and conclusion . . . . . . . . . . . . . . . . . . . . . . 7

3 Staging the more compact CPS transformation 7

4 More compact CPS transformations in one pass 8

5 Conclusion and issues 10

List of Figures

1 A family of one-pass, call-by-value CPS transformations à la Plotkin 9 2 A family of one-pass, call-by-value CPS transformations à la Fischer 9

1 Introduction

1.1 Continuation-passing style (CPS)

The meaning of a λ-term, in general, depends on its evaluation order. Evaluationorder independence was one of the motivations for continuations [14, 21], and continuation-passing style was developed as an evaluation-order independent λ-encoding of λ-terms [4, 13]. In this λ-encoding, each evaluation context is represented by a λ-abstraction, called a continuation, and each λ-abstraction is passed a continuation in addition to its usual argument. All intermediate results are sent to a continuation and thus all calls are tail-calls. This λ-encoding gives rise to a variety of continuation-passing styles, whose structure is a subject of study in itself [8, 15, 20].

1.2 The CPS transformation

The format of CPS λ-terms was soon noticed to be of interest for the compiler writer [18], which in turn fostered interest in automating the transformation of λ-terms into CPS. Over the last twenty years, a wide body of CPS transformations has thus been developed for various purposes, e.g., to compile and to analyze programs, and to generate compilers [1, 6, 10, 17, 18, 22].

The naïve λ-encoding into CPS, however, generates a quite impressive inflation of lambdas, most of which form administrative redexes that can be safely reduced. Administrative reductions yield CPS terms corresponding to what one could write by hand. It has therefore become a challenge to eliminate as many administrative redexes as possible, at CPS-transformation time.

1.3 Sabry and Felleisen’s optimization

In their article “Reasoning about Programs in Continuation-Passing Style” [16], Sabry and Felleisen present a CPS transformation that yields more compact terms than existing CPS transformations. For example [16, Footnote 6], CPStransforming

((λx.λy.x) a) b

where a and b are variables, yields the term

λk.((λx.((λy.k x) b)) a)

whereas earlier transformations, such as Steele’s [18] or Danvy and Filinski’s [3], yield the more voluminous term

λk.((λx.λk_{1}.(k_{1} (λy.λk_{2}.k_{2} x))) a (λm.m b k)).

Sabry and Felleisen’s optimization relies on using Fischer’s CPS (where continuations occur first, as in λk.λx.e), whereas earlier transformations use Plotkin’s CPS (where values occur first, as in λx.λk.e).

1.4 This article

Section 2 reviews administrative reductions in the CPS transformation and characterizes Sabry and Felleisen’s optimization, independent of the relative positions of values and continuations in CPS terms (i.e., both for Fischer’s and Plotkin’s CPS). Section 3 constructs a similarly compact CPS transformation by composing an uncurrying phase and an ordinary CPS transformation. Section 4 integrates the optimization in a context-insensitive, one-pass CPS transformation. Section 5 concludes.

2 Administrative reductions in the CPS transformation

2.1 Context-insensitive administrative reductions

Appel, Danvy and Filinski, and Wand each independently developed a “onepass” CPS transformation for call by value [1, 3, 22]. This CPS transformation relies on a context-free characterization of administrative reductions, i.e., a characterization that is independent of any source term. This one-pass transformation, shown below for Plotkin’s CPS, is formulated with a static, context-free distinction between (translation-time) administrative reductions and (run-time) reductions, using a two-level λ-calculus [3, 12].

[[·]]_{p} : Λ → (Λ → Λ) → Λ
[[x]]_{p} = \overline{λ}κ.κ \overline{@} x
[[λx.e]]_{p} = \overline{λ}κ.κ \overline{@} (\underline{λ}x.\underline{λ}k.[[e]]_{p} \overline{@} (\overline{λ}t.k \underline{@} t))
[[e_{0} e_{1}]]_{p} = \overline{λ}κ.[[e_{0}]]_{p} \overline{@} (\overline{λ}t_{0}.[[e_{1}]]_{p} \overline{@} (\overline{λ}t_{1}.(t_{0} \underline{@} t_{1}) \underline{@} (\underline{λ}v.κ \overline{@} v)))

“\underline{λ}” and “\underline{@}” denote hygienic abstract-syntax constructors and “\overline{λ}” and “\overline{@}” denote translation-time abstractions and (infix) applications, respectively. A λ-term e : Λ is CPS-transformed with

\underline{λ}k.[[e]]_{p} \overline{@} (\overline{λ}t.k \underline{@} t).

The corresponding one-pass transformation for Fischer’s CPS is as follows.

[[·]]_{f} : Λ → (Λ → Λ) → Λ
[[x]]_{f} = \overline{λ}κ.κ \overline{@} x
[[λx.e]]_{f} = \overline{λ}κ.κ \overline{@} (\underline{λ}k.\underline{λ}x.[[e]]_{f} \overline{@} (\overline{λ}t.k \underline{@} t))
[[e_{0} e_{1}]]_{f} = \overline{λ}κ.[[e_{0}]]_{f} \overline{@} (\overline{λ}t_{0}.[[e_{1}]]_{f} \overline{@} (\overline{λ}t_{1}.(t_{0} \underline{@} (\underline{λ}v.κ \overline{@} v)) \underline{@} t_{1}))

A λ-term e : Λ is CPS-transformed with

\underline{λ}k.[[e]]_{f} \overline{@} (\overline{λ}t.k \underline{@} t).

2.2 Context-sensitive administrative reductions

Sabry and Felleisen (1) tag all the “new” lambdas introduced by the CPS transformation, (2) reduce systematically the β-redexes with a tagged lambda, and (3) untag the remaining tagged lambdas:

[[x]] = \overline{λ}k.k x
[[λx.e]] = \overline{λ}k.k (\overline{λ}k.λx.[[e]] k)
[[e_{0} e_{1}]] = \overline{λ}k.[[e_{0}]] (\overline{λ}t_{0}.[[e_{1}]] (\overline{λ}t_{1}.t_{0} k t_{1}))

A λ-term e is CPS-transformed with

[[e]].

An administrative reduction amounts to reducing a β-redex where the λ-abstr-action is tagged.

This three-pass CPS transformation resembles much the Fischer-style onepass CPS transformation of Section 2.1, with three exceptions:

Form: it does not use @ for applications, is more implicit by not underlining abstract-syntax constructors, and η-reduces continuations.

Content: it is a first-order rewriting system whereas the one-pass transformation is a higher-order one.

Plus: it contains one more overlined λ-abstraction, namely the one declaring the continuation of a λ-abstraction.

The extra overline makes administrative reductions context-sensitive, as illustrated below:

[[λx.((λy.y) x)]] = \overline{λ}k.k (\overline{λ}k.λx.(\overline{λ}k.k (\overline{λ}k.λy.(\overline{λ}k.k y) k)) \overline{λ}t_{0}.(\overline{λ}k.k x) \overline{λ}t_{1}.t_{0} k t_{1}) ⟶\overline{β}^{+} \overline{λ}k.k (\overline{λ}k.λx.(\overline{λ}k.λy.k y) k x) ⟶\overline{β} \overline{λ}k.k (\overline{λ}k.λx.(λy.k y) x)

The term \overline{λ}k.λx.... arises from the transformation of λx.... and cannot be administratively reduced. The term \overline{λ}k.λy.... arises from the transformation of λy.... and can be administratively reduced.

In contrast, in a context-insensitive one-pass CPS transformation, all overlined λ-abstractions are guaranteed to occur in an overlined application (and thus there is no need for post-erasure). A context-sensitive CPS transformation thus can perform more administrative reductions than a context-insensitive one.

Furthermore, we can precisely locate the extra gain: for source β-redexes. Given a source β-redex, one can actually substitute the continuation of the application for the continuation of the abstraction:

(λx.e[c/k]) t_{1}

thereby enabling further administrative reductions inside e.

This reduction is not accounted for in a (say, Plotkin-style) one-pass CPS transformation, since in the particular case where t_{0} denotes \underline{λ}x.\underline{λ}k.e, one does not simplify

(t_{0} \underline{@} t_{1}) \underline{@} c

into

(\underline{λ}x.e[c/k]) \underline{@} t_{1}.

The reduction thus yields more compact CPS counterparts of source βredexes, in that the translated λ-abstractions are not explicitly passed any continuation when they occur in a β-redex.^{1}

On the other hand, a similar phenomenon occurs for let expressions, as reviewed next.

2.3 CPS transformation of let expressions

The CPS transformation of let expressions reads as follows:

[[let x = e′ in e]] = \overline{λ}κ.[[e′]]\overline{λ}t′.\underline{let} x = t′ \underline{in} [[e]]κ

In words, e is in tail-position in the let expression, and is CPS-transformed with respect to the same κ as the let expression. This technique is instrumental in continuation-based partial evaluation [11].

Seeing let expressions as syntactic sugar for β-redexes, it appears clearly that the context-sensitive administrative reduction includes the standard let optimization, independently of whether continuations are put first or last. This administrative reduction, however, yields more.

2.4 CPS transformation of embedded β-redexes

Extra mileage is obtained for fully applied (curried) λ-abstractions. CPStransforming the curried application of a “n-ary” λ-abstraction to n arguments relocates the continuation of the application to the body of the λ-abstraction.

[[(λx_{1}....λx_{n}.e) e_{1}... e_{n}]] = \overline{λ}κ.[[e_{1}]] \overline{@} (\overline{λ}t_{1}....[[e_{n}]] \overline{@} (\overline{λ}t_{n}.(\underline{λ}x_{n}....(\underline{λ}x_{1}.[[e]] \overline{@} κ) \underline{@} t_{1}...) \underline{@} t_{n})...)

This extra mileage is independent of whether continuations are put first or last. As a net effect, a term such as

(λf.λg.λx.f x (g x)) (a b) c (d e)

1As Shivers puts it [17] and can be read off their type, the translated λ-abstractions are promoted to continuations.

where a, b, c, d, and e are variables, is CPS transformed into (letting continuations occur last)

λk.a b (λf.(λg.d e (λx.f x (λv_{1}.g x (λv_{2}.v_{1} v_{2} k)))) c).

Observe how the λ-abstractions λf.... and λx.... end up as the continuations of the applications (a b) and (d e), and how the application of λg.... to c survives in the CPS term.

Letting continuations occur first would yield a similar term:

λk.a (λf.(λg.d (λx.f (λv_{1}.g (λv_{2}.v_{1} k v_{2}) x) x) e) c) b.

2.5 Summary and conclusion

A CPS transformation with context-sensitive administrative reductions yields more compact CPS terms because it exposes more administrative redexes. The extra administrative reductions affect nested β-redexes corresponding to fully applied curried λ-abstractions, and reduce continuation-passing by promoting the inner λ-abstractions to continuations. These extra administrative reductions can be carried out independently of whether continuations occur first or last in CPS terms.

3 Staging the more compact CPS transformation

Sabry and Felleisen [16, Definition 7, page 306] identify a reduction β_{lift} moving the context of a β-redex into the body of the corresponding λ-abstraction:^{2}

E[(λx.M)N] ⟶ \begin{matrix}(λx.E[M])N \\ where E ≠ [ ] and x ∉ FV (E) \end{matrix} (β_{lift})

They also pointed out that CPS-transforming a term e and mapping the result back to direct style yields a term in β_{lift}-normal form.

But a term in β_{lift}-normal form does not give rise to the extra contextsensitive administrative reduction of Section 2. Therefore, the extra power of the context-sensitive CPS transformation is solely due to β_{lift}.

The more compact CPS transformation can thus be staged as follows:

1. a phase uncurrying (and appropriately renaming, if need be) all β-redexes

(λx_{1}....λx_{n}.e) e_{1}... e_{n}

into embedded let expressions let x_{1} = e_{1} in let x_{2} = e_{2} in ... \begin{matrix}let x_{n} = e_{n} \\ in e \end{matrix} 2. an ordinary, context-insensitive CPS transformation (either à la Plotkin

2The transitive closure of β_{lift} is a generalized reduction in the sense of Bloo, Kamareddine, and Nederpelt [2].

or à la Fischer) handling let expressions.

The benefit of this staging, we believe, is three-fold: (1) it clarifies the extra compaction; (2) it extends a context-insensitive, one-pass CPS transformation; and (3) it suggests how to obtain even more compact terms. Indeed, in the same fashion as control-flow analysis can be used to locate the application sites of curried λ-abstractions in order to uncurry them [1, 7], the CPS transformation can benefit from control-flow information to promote more functions to continuations.

4 More compact CPS transformations in one pass

Promoting functions into continuations compromises context independence in the CPS transformation, since how to CPS-transform a λ-abstraction depends on whether it occurs in a β-redex or not. Fortunately, it does so in a very regular way, which makes it possible to derive a family of one-pass CPS transformations indexed by positions in the current context.

[figure: @^{0}; @^{1}; @^{n}; λ^{n−1}; λ^{n−2}]

Indexing the transformation functions with the lexical position of their argument yields the one-pass CPS transformation à la Plotkin of Figure 1. A λ-term e : Λ is CPS-transformed with

\underline{λ}k.[[e]]^{0} \overline{@} (\overline{λ}t.k \underline{@} t).

Similarly, a one-pass CPS transformation à la Fischer is displayed in Figure 2.

Ψ^{0} v = \begin{aligned}v & : & τ_{0} \\ & & where τ_{0} = Λ. \end{aligned}
Ψ^{n+1} v = \overline{λ}t.\overline{λ}κ.(t \underline{@} v) \underline{@} (\underline{λ}v′.κ \overline{@} (Ψ^{n} v′))

: τ_{n+1}

where τ_{n+1} = Λ → (τ_{n} → Λ) → Λ.
[[·]]^{n} : Λ → (τ_{n} → Λ) → Λ
[[x]]^{n} = \overline{λ}κ.κ \overline{@} (Ψ^{n} x)
[[λx.e]]^{0} = \overline{λ}κ.κ \overline{@} (\underline{λ}x.\underline{λ}k.[[e]]^{0} \overline{@} (\overline{λ}t.k \underline{@} t))
[[λx.e]]^{n+1} = \overline{λ}κ.κ \overline{@} (\overline{λ}t.\overline{λ}κ′.(\underline{λ}x.[[e]]^{n} \overline{@} κ′) \underline{@} t)
[[e_{0} e_{1}]]^{n} = \overline{λ}κ.[[e_{0}]]^{n+1} \overline{@} (\overline{λ}t_{0}.[[e_{1}]]^{0} \overline{@} (\overline{λ}t_{1}.(t_{0} \overline{@} t_{1}) \overline{@} κ))

Figure 1: A family of one-pass, call-by-value CPS transformations à la Plotkin

Φ^{0} v = \begin{aligned}v & : & τ_{0} \\ & & where τ_{0} = Λ. \end{aligned}
Φ^{n+1} v = \overline{λ}κ.v \underline{@} (\underline{λ}v′.κ \overline{@} (Φ^{n} v′))
: \begin{matrix}τ_{n+1} \\ where τ_{n+1} = (τ_{n} → Λ) → Λ. \end{matrix}
[[·]]^{n} : Λ → (τ_{n} → Λ) → Λ
[[x]]^{n} = \overline{λ}κ.κ \overline{@} (Φ^{n} x)
[[λx.e]]^{0} = \overline{λ}κ.κ \overline{@} (\underline{λ}k.\underline{λ}x.[[e]]^{0} \overline{@} (\overline{λ}t.k \underline{@} t))
[[λx.e]]^{n+1} = \overline{λ}κ.κ \overline{@} (\overline{λ}κ′.\underline{λ}x.[[e]]^{n} \overline{@} κ′)
[[e_{0} e_{1}]]^{n} = \overline{λ}κ.[[e_{0}]]^{n+1} \overline{@} (\overline{λ}t_{0}.[[e_{1}]]^{0} \overline{@} (\overline{λ}t_{1}.(t_{0} \overline{@} κ) \underline{@} t_{1}))

Figure 2: A family of one-pass, call-by-value CPS transformations à la Fischer

[[·]]^{0} is applied to the root of a term (i.e., to the body of a λ-abstraction or to the expression in position of argument in an application). For n > 0, [[·]]^{n} is applied to an expression in position of function in an application. n is the depth of the expression since the closest root, as in the picture above. Ψ (resp. Φ) coerces a syntactic object into a translation-time one.

The transformation based on these families of functions can be proven correct by a simulation theorem similar to Plotkin’s [13]. The correctness criterion is a relation between the transformation of the result of an expression and the result of the transformation of it, i.e., (noting contextual equivalence with ∼)

e ⟶^{∗} v implies [[e]]^{0} λa.a ⟶^{∗} v′ and v′ ∼ [[v]]^{0} λa.a

as well as preservation of non-termination and of getting stuck.

Reflecting the context dependence of both CPS transformations, the twolevel specifications in Figures 1 and 2 are not themselves simply typed. Instead, they are dependently typed and define two families of simply typed two-level specifications. Each of these families produces simply-typed two-level λ-terms, that can be statically (i.e., administratively) reduced in one pass.

Figures 1 and 2 can be programmed in a dependently typed language and also in Scheme, if one treats the indices as arguments.

5 Conclusion and issues

In their study of CPS programs [16], Sabry and Felleisen needed a CPS transformation that would perform more administrative reductions than the ones already available [1, 3, 6, 22]. We have identified the extra power of this CPS transformation: a context-sensitive administrative reduction enabling a more effective treatment of β-redexes which corresponds to Bloo, Kamareddine, and Nederpelt’s notion of generalized reduction. This treatment turns out to be independent of the relative positions of values and continuations. The resulting CPS transformation can be factored into (1) a first-order uncurrying phase and (2) a CPS transformation with context-insensitive administrative reductions. We have also presented two one-pass CPS transformations embodying the extra compaction and generalizing the corresponding one-pass CPS transformations à la Plotkin and à la Fischer. They can be adapted mutatis mutandis for encoding λ-terms into monadic normal form [9], A-normal form [5, Figure 9], nqCPS, etc., including β_{lift}.

Acknowledgements: The first author is grateful to Matthias Felleisen, Andrzej Filinski, John Hatcliff, and Amr Sabry for discussions and comments on this topic and these transformations in June and July 1993, at CMU. Kristoffer Rose wanted to see the dependent types of Figures 1 and 2 spelled out. Thanks are also due to the reviewers and to Julia Lawall for perceptive comments.

References

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

[2] Roel Bloo, Fairouz Kamareddine, and Rob Nederpelt. The Barendregt cube with definitions and generalised reduction. Information and Computation, 126(2):123–143, 1996.

[3] Olivier Danvy and Andrzej Filinski. Representing control, a study of the CPS transformation. Mathematical Structures in Computer Science, 2(4):361–391, December 1992.

[4] Michael J. Fischer. Lambda-calculus schemata. In Talcott [19], pages 259–288. An earlier version appeared in an ACM Conference on Proving Assertions about Programs, SIGPLAN Notices, Vol. 7, No. 1, January 1972.

[5] Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. The essence of compiling with continuations. In David W. Wall, editor, Proceedings 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.

[6] Daniel P. Friedman, Mitchell Wand, and Christopher T. Haynes. Essentials of Programming Languages. The MIT Press and McGraw-Hill, 1991.

[7] John Hannan and Patrick Hicks. Higher-order unCurrying. Higher-Order and Symbolic Computation, 13(3):179–218, 2000.

[8] John Hatcliff. The Structure of Continuation-Passing Styles. PhD thesis, Department of Computing and Information Sciences, Kansas State University, Manhattan, Kansas, June 1994.

[9] 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.

[10] David Kranz, Richard Kesley, Jonathan Rees, Paul Hudak, Jonathan Philbin, and Norman Adams. Orbit: An optimizing compiler for Scheme. In Proceedings of the ACM SIGPLAN’86 Symposium on Compiler Construction, pages 219–233, Palo Alto, California, June 1986. ACM Press.

[11] Julia L. Lawall and Olivier Danvy. Continuation-based partial evaluation. In Carolyn L. Talcott, editor, Proceedings of the 1994 ACM Conference on Lisp and Functional Programming, LISP Pointers, Vol. VII, No. 3, Orlando, Florida, June 1994. ACM Press.

[12] Flemming Nielson and Hanne Riis Nielson. Two-Level Functional Languages, volume 34 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1992.

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

[14] John C. Reynolds. The discoveries of continuations. In Talcott [19], pages 233–247.

[15] Amr Sabry. The Formal Relationship between Direct and Continuation-Passing Style Optimizing Compilers: A Synthesis of Two Paradigms. PhD thesis, Computer Science Department, Rice University, Houston, Texas, August 1994. Technical report TR94-242.

[16] Amr Sabry and Matthias Felleisen. Reasoning about programs in continuation-passing style. In Talcott [19], pages 289–360.

[17] Olin Shivers. Control-Flow Analysis of Higher-Order Languages or Taming Lambda. PhD thesis, School of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania, May 1991. Technical Report CMU-CS-91-145.

[18] Guy L. Steele Jr. Rabbit: A compiler for Scheme. Technical Report AI-TR-474, Artificial Intelligence Laboratory, Massachusetts Institute of Technology, Cambridge, Massachusetts, May 1978.

[19] Carolyn L. Talcott, editor. Special issue on continuations (Part I), Lisp and Symbolic Computation, Vol. 6, Nos. 3/4, December 1993.

[20] Hayo Thielecke. Categorical Structure of Continuation Passing Style. PhD thesis, University of Edinburgh, Edinburgh, Scotland, 1985. ECS-LFCS-97-376.

[21] Christopher P. Wadsworth. Continuations revisited. Higher-Order and Symbolic Computation, 13(1/2):131–133, 2000.

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

Recent BRICS Report Series Publications

RS-00-35 Olivier Danvy and Lasse R. Nielsen. CPS Transformation of Beta-Redexes. December 2000. 12 pp. Appears in Sabry, editor, 3rd ACM SIGPLAN Workshop on Continuations, CW ’01 Proceedings, Association for Computing Machinery (ACM) Technical report 545, Computer Science Department, Indiana University, 2001, pages 35–39.

RS-00-34 Olivier Danvy and Morten Rhiger. A Simple Take on Typed Abstract Syntax in Haskell-like Languages. December 2000. 25 pp. Appears in Kuchen and Ueda, editors, Fifth International Symposium on Functional and Logic Programming, FLOPS ’01 Proceedings, LNCS 2024, 2001, pages 343–358.

RS-00-33 Olivier Danvy and Lasse R. Nielsen. A Higher-Order Colon Translation. December 2000. 17 pp. Appears in Kuchen and Ueda, editors, Fifth International Symposium on Functional and Logic Programming, FLOPS ’01 Proceedings, LNCS 2024, 2001, pages 78–91.

RS-00-32 John C. Reynolds. The Meaning of Types — From Intrinsic to Extrinsic Semantics. December 2000. 35 pp. A shorter version of this report describing a more limited language appears in Annabelle McIver and Carroll Morgan (eds.) Essays on Programming Methodology, Springer-Verlag, New York, 2001.

RS-00-31 Bernd Grobauer and Julia L. Lawall. Partial Evaluation of Pattern Matching in Strings, revisited. November 2000. 48 pp.

RS-00-30 Ivan B. Damgård and Maciej Koprowski. Practical Threshold RSA Signatures Without a Trusted Dealer. November 2000. 14 pp. Appears in Pfitzmann, editor, Advances in Cryptology: International Conference on the Theory and Application of Cryptographic Techniques, EUROCRYPT ’01 Proceedings, LNCS 2045, 2001, pages 152–165.

RS-00-29 Luigi Santocanale. The Alternation Hierarchy for the Theory of μ-lattices. November 2000. 44 pp. Extended abstract appears in Abstracts from the International Summer Conference in Category Theory, CT2000, Como, Italy, July 16–22, 2000. Appears in Theory and Applications of Categories, Volume 9, CT2000, pp. 166-197.