BRICS RS-02-36 Damian & Danvy: CPS Transformation of Flow Information, Part II: Administrative Reductions BRICS

Basic Research in Computer Science

CPS Transformation of Flow Information Part II: Administrative Reductions

Daniel Damian Olivier Danvy BRICS Report Series RS-02-36 ISSN 0909-0878 August 2002 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2002, Daniel Damian & 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/36/

CPS Transformation of Flow Information,

Part II: Administrative Reductions ^{∗}

Daniel Damian^{†} and Olivier Danvy

BRICS^{‡}

Department of Computer Science University of Aarhus^{§}

August 13, 2000 (updated: August 9, 2001 and August 6, 2002)

Abstract

We characterize the impact of a linear β-reduction on the result of a controlflow analysis. (By “a linear β-reduction” we mean the β-reduction of a linear λ-abstraction, i.e., of a λ-abstraction whose parameter occurs exactly once in its body.)

As a corollary, we consider the administrative reductions of a Plotkin-style transformation into continuation-passing style (CPS), and how they affect the result of a constraint-based control-flow analysis and, in particular, the least element in the space of solutions. We show that administrative reductions preserve the least solution. Preservation of least solutions solves a problem that was left open in Palsberg and Wand’s article “CPS Transformation of Flow Information.”

Together, Palsberg and Wand’s article and the present article show how to map in linear time the least solution of the flow constraints of a program into the least solution of the flow constraints of the CPS counterpart of this program, after administrative reductions. Furthermore, we show how to CPS transform control-flow information in one pass.

∗To appear in the Journal of Functional Programming.

† Current affiliation: LION Bioscience Ltd., Compass House, 80-82 Newmarket Road, Cambridge CB5 8DZ, UK.

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

§ Ny Munkegade, Building 540, DK-8000 Aarhus C, Denmark Email:{damian,danvy}@brics.dk

1 Background and introduction

Since their inception, over thirty years ago [13], continuations and the transformation into continuation-passing style (CPS) have been the topic of much study, ranging from semantics and logic to implementations of sequential, concurrent, and distributed programming languages and systems. Fifteen years ago [9, 16], Meyer and Wand noticed that the CPS transformation preserves types and they constructed a CPS transformation of types.

[figure: type; CPS transformation; of types; type; direct-style program; type inference; CPS transformation; of terms; CPS program; type inference]

Over the last couple of years, Palsberg and Wand have extended this observation to flow types and the flow information gathered by a control-flow analysis [11], designing a CPS transformation of flow information.

[figure: flow information; CPS transformation; of flow; flow information; direct-style program; flow analysis; CPS transformation; of terms; CPS program; flow analysis]

Independently, and with a different motivation, we have also designed a CPS transformation of flow information for control flow and binding times [1–3]. The two CPS transformations of flow information correspond to two different takes on the CPS transformation of λ-terms:

CPS with administrative redexes administrative

reductions [figure]

[figure]

direct style

CPS transformation

[figure]

transformation into monadic style [figure]

[figure]

CPS without administrative redexes

monadic normal form introduction of continuations

[figure]

The CPS transformation is Plotkin’s [12]. It is a first-order, compositional rewriting system generating numerous administrative redexes that need to be post-reduced in practice [15]. Alternatively [5, 14], the CPS transformation can be staged into a transformation into monadic normal form followed by an introduction of continuations.

The two CPS transformations of flow information can be depicted as follows.

CPS with administrative redexes

this work [figure]

[figure]

direct style Palsberg & Wand, JFP’02

[figure]

Damian & Danvy, JFP’02 [figure]

[figure]

CPS without administrative redexes

monadic normal form Damian & Danvy, ICFP’00

[figure]

Palsberg and Wand show how to construct in linear time the flow information corresponding to a CPS program obtained through a Plotkin-style CPS transformation [11, 12]. The resulting programs contain all administrative redexes induced by Plotkin’s transformation. Therefore, the corresponding CPS information of flow also contains spurious information which accounts for the extraneous λ-abstractions and their flow. The problem of eliminating this spurious information is open.

Damian and Danvy show how to construct in linear time the flow information corresponding to the introduction of continuations, starting from monadic normal forms [2, 5]. They also show how to construct in linear time the flow information corresponding to the transformation into monadic normal forms [1, 3].

In this work, we complete the picture above by showing how to perform in linear time administrative reductions on CPS-transformed programs (Section 4). Our result hinges on linear reductions (Section 3). But first, we present the source language and a constraint-based control-flow analysis (Section 2).

2 Preliminaries

2.1 The source language

Input terms are given by the grammar in Figure 1. Terms are annotated with distinct labels taken from a countable set Lab. Each λ-abstraction is annotated with a distinct label π from a set Lam, and we assume that there exists a bijection between λabstractions and their labels.

e ∈ Exp ::= x | n | e_{1}^{ℓ_{1}} e_{2}^{ℓ_{2}} | if0 e^{ℓ} e_{0}^{ℓ_{0}} e_{1}^{ℓ_{1}} | λ^{π}x.e^{ℓ}
π ∈ Lam  (λ-abstraction labels)
ℓ ∈ Lab  (term labels)
n ∈ Lit  (integer literals)

Figure 1: The language of labeled λ-terms

The language has a standard call-by-value semantics, which we leave unspecified. A program p is a closed labeled expression e^{ℓ}.

Definition 2.1. A properly labeled expression is a labeled expression in which all labels are distinct and all variables are distinct.

2.2 Control-flow analysis

We consider a constraint-based control-flow analysis. We use the same notations and definitions as in Nielson, Nielson and Hankin’s recent textbook on program analysis [10].

Given a program p, the control-flow analysis is defined as a relation ⊨_{p} whose functionality is displayed in Figure 2.

Lam^{p}  The set of λ-abstraction labels in p
Var^{p}  The set of identifiers in p
Lab^{p}  The set of term labels in p
Val^{p} = P(Lam^{p})  Abstract values
Ĉ ∈ Cache_{p} = Lab^{p} → Val^{p} Abstract cache
ρ̂ ∈ Env_{p} = Var^{p} → Val^{p} Abstract environment
⊨_{p} ⊆ (Cache_{p} × Env_{p}) × Lab^{p}

Figure 2: Control-flow analysis relation for a program p: functionality

A solution of the analysis of p is a pair (Ĉ, ρ̂) such that (Ĉ, ρ̂) ⊨ p. The set of solutions of the analysis is ordered by the natural pointwise ordering of functions, and has a least element. This property ensures the existence of a least solution of the analysis of p. The analysis relation is defined inductively on the syntax as defined in Figure 3.

(Ĉ, ρ̂) ⊨_{p} n^{ℓ}  ⟺ true
(Ĉ, ρ̂) ⊨_{p} x^{ℓ}  ⟺ ρ̂(x) ⊑ Ĉ(ℓ)
(Ĉ, ρ̂) ⊨_{p} (λ^{π}x.e^{ℓ})^{ℓ_{1}}  ⟺ π ∈ Ĉ(ℓ_{1}) ∧ (Ĉ, ρ̂) ⊨_{p} e^{ℓ}
(Ĉ, ρ̂) ⊨_{p} (e_{1}^{ℓ_{1}} e_{2}^{ℓ_{2}})^{ℓ}  ⟺ (Ĉ, ρ̂) ⊨_{p} e_{1}^{ℓ_{1}} ∧ (Ĉ, ρ̂) ⊨_{p} e_{2}^{ℓ_{2}}∧

∀λ^{π}x.e_{0}^{ℓ_{0}} ∈ Ĉ(ℓ_{1}).\begin{matrix}Ĉ(ℓ_{2}) ⊆ ρ̂(x) ∧ \\ Ĉ(ℓ_{0}) ⊆ Ĉ(ℓ) \end{matrix}

(Ĉ, ρ̂) ⊨_{p} (if0 e^{ℓ} e_{0}^{ℓ_{0}} e_{1}^{ℓ_{1}})^{ℓ_{2}} ⟺ \begin{matrix}(Ĉ, ρ̂) ⊨_{p} e^{ℓ} ∧ (Ĉ, ρ̂) ⊨_{p} e_{0}^{ℓ_{0}} ∧ (Ĉ, ρ̂) ⊨_{p} e_{1}^{ℓ_{1}} ∧ \\ Ĉ(ℓ_{0}) ⊆ Ĉ(ℓ_{2}) ∧ Ĉ(ℓ_{1}) ⊆ Ĉ(ℓ_{2}) \end{matrix}

Figure 3: Control-flow analysis relation for a program p: definition

3 Linear reductions

We observe that linear reductions preserve flow information. A linear reduction is a β-reduction in which the λ-abstraction in the function position is linear, i.e., such that it uses its argument once and only once. Let us formalize the notion of linear reduction using linear contexts.

Definition 3.1. A linear context is a labeled expression with a unique hole [·]. Linear contexts are defined by the grammar:

E ::= [·] | x^{ℓ} | n^{ℓ} | (E e_{2}^{ℓ_{2}})^{ℓ} | (e_{1}^{ℓ_{1}} E)^{ℓ} |
(if0 E e_{0}^{ℓ_{0}} e_{1}^{ℓ_{1}})^{ℓ} | (if0 e^{ℓ} E e_{1}^{ℓ_{1}})^{ℓ_{0}} | (if0 e^{ℓ} e_{0}^{ℓ_{0}} E)^{ℓ_{1}} |
(λ^{π}x.E)^{ℓ}

Given a linear context E and a labeled expression e^{ℓ}, we use E[e^{ℓ}] to denote the context E with the hole [·] replaced with e^{ℓ}. It is trivial to see that E[e^{ℓ}] is a well-formed expression. Note that pluging as defined here does not avoid variable capturing. We use plugging however only in the context of properly-labeled programs, where there is no danger of variable capture.

We also use FV (e) to denote the set of free variables of the expression e. This notation naturally extends to contexts: given the context E, by definition FV (E) = FV (E[n]), where n is an arbitrary literal. We use L as the function extracting the label of an expression. By definition, for any labeled expression e^{ℓ}, L(e^{ℓ}) = ℓ.

Definition 3.2. A labeled λ-abstraction (λ^{π}x.e^{ℓ_{1}})^{ℓ_{2}} is linear if and only if is properly labeled and e^{ℓ_{1}} contains a unique occurrence of x, i.e., if there exists a linear context E such that x ∉ FV (E) and e = E[x^{ℓ}] for some label ℓ.

Definition 3.3. A linear redex is a β-redex (λx.e_{1}) e_{2} such that λx.e_{1} is a linear λ-abstraction.

Definition 3.4. A linear reduction is the β-reduction of a linear redex.

Example:

((λ^{π}x.E[x^{ℓ}])^{ℓ_{1}} e^{ℓ_{2}})^{ℓ_{3}} → E[e^{ℓ_{2}}]

where E is a linear context where x does not occur free. Note that such a reduction might not necessarily be sound wrt. call-by-value semantics. Nevertheless, we show that it does not affect the result of control-flow analysis. In any case, we treat linear reductions in CPS, which is evaluation-order independent [12].

4 Control-flow analysis and linear reduction

We show that performing a linear reduction does not alter the results of the analysis of a properly labeled program. More precisely, we show that, given a properly labeled program which contains a linear β-redex, control-flow analysis yields strictly equivalent results before and after performing a linear β-reduction.

We are given a program that contains a linear redex and the least solution of its analysis. The goal of this section is to construct the least solution of the analysis of this program after a linear β-reduction.

Let p be a properly labeled program containing a linear β-redex. Therefore there exist two linear contexts E and E_{1}, an expression e, a fresh variable x, and labels π, ℓ_{0}, ℓ_{1}, ℓ_{2} and ℓ_{3} such that

p = E[((λ^{π}x.E_{1}[x^{ℓ_{0}}])^{ℓ_{1}} e^{ℓ_{2}})^{ℓ_{3}}]

and x ∉ FV (E). Let then

p′ = E[E_{1}[e^{ℓ_{2}}]]

be the program p with the linear redex above reduced. It is immediate to see that p′ is also a properly labeled program.

In the rest of this section, we define a monotone function F_{p} which, given a solution of the analysis of p, constructs a solution of the analysis of p′. We then define a reverse function G_{p}, monotone as well, which, given a solution of the analysis of p′, constructs a solution of the analysis of p. Using the two functions and their monotonicity, we show that the best solution for p is transformed into the best solution for p′. We then show how to construct in linear time the least solution of the analysis of p′ from the least solution of the analysis of p.

4.1 Flow constructions

For the programs p and p′ defined as above, by construction,

• Lab^{p} = Lab^{p′} ∪ {ℓ_{0}, ℓ_{1}, ℓ_{3}},

• Lam^{p} = Lam^{p′} ∪ {π}, and

• Var^{p} = Var^{p′} ∪ {x}.

We define a function F_{p} : (Cache_{p} × Env_{p}) → (Cache_{p′} × Env_{p′}) as F_{p}(Ĉ, ρ̂) = (Ĉ|_{Lam}_{p′} , ρ̂|_{Lam}_{p′}). Obviously, F_{p} is a projection function and it is monotone with respect to the ordering of solutions.

We define a reverse function G_{p} : (Cache_{p′} ×Env_{p′}) → (Cache_{p} ×Env_{p}) as follows. G_{p}(Ĉ′, ρ′) = (Ĉ, ρ̂) such that:

• for all ℓ ∈ Lab^{p′}, Ĉ(ℓ) = Ĉ′(ℓ); Ĉ(ℓ_{3}) = Ĉ′(L(E_{1}[e^{ℓ_{2}}])); Ĉ(ℓ_{0}) = ρ̂(x) = Ĉ′(ℓ_{2}); Ĉ(ℓ_{1}) = {π}; and

• for all y ∈ Var^{p′}, ρ̂(y) = ρ′(y).

Obviously, G_{p} is an embedding function and it is monotone as well.

Lemma 4.1. Let (Ĉ, ρ̂) ∈ (Cache_{p} × Env_{p}) such that (Ĉ, ρ̂) ⊨_{p} p. Then F_{p}(Ĉ, ρ̂) ⊨_{p′} p′.

Proof. Let (Ĉ′, ρ′) = F_{p}(Ĉ, ρ̂). We show that (Ĉ′, ρ′) ⊨_{p′} p′. The proof has two steps:

i) A proof of the fact that (Ĉ′, ρ′) ⊨_{p′} E_{1}[e^{ℓ_{2}}]. The proof is by structural induction on the context E_{1}, using the assumption that (Ĉ′, ρ′) ⊨_{p′} E_{1}[x^{ℓ_{0}}].

ii) A proof of the fact that (Ĉ′, ρ′) ⊨_{p′} E[E_{1}[e^{ℓ_{2}}]]. The proof is by structural induction on the context E.

Lemma 4.2. Let (Ĉ′, ρ′) ∈ (Cache_{p′} × Env_{p′}) such that (Ĉ′, ρ′) ⊨_{p′} p′. Then G_{p}(Ĉ′, ρ′) ⊨_{p} p.

Proof. Let (Ĉ, ρ̂) = G_{p}(Ĉ′, ρ′). We show that (Ĉ, ρ̂) ⊨_{p} p. The proof has three steps:

i) A proof of the fact that (Ĉ, ρ̂) ⊨_{p} E_{1}[x^{ℓ_{0}}]. The proof is by structural induction on the context E_{1}, using the assumption that (Ĉ′, ρ′) ⊨_{p′} E_{1}[e^{ℓ_{2}}].

ii) A proof of the fact that (Ĉ, ρ̂) ⊨_{p} ((λ^{π}x.E_{1}[x^{ℓ_{0}}])^{ℓ_{1}} e^{ℓ_{2}})^{ℓ_{3}}. Using i), the proof amounts to showing that a small set of constraints are satisfied.

iii) A proof of the fact that (Ĉ, ρ̂) ⊨_{p} E[((λ^{π}x.E_{1}[x^{ℓ_{0}}])^{ℓ_{1}} e^{ℓ_{2}})^{ℓ_{3}}]. The proof is by structural induction on the context E.

Lemma 4.3. Let (Ĉ, ρ̂) be the least solution of the analysis of p. Let (Ĉ′, ρ′) be the least solution of the analysis of p′. Then F_{p}(Ĉ, ρ̂) = (Ĉ′, ρ′) and G_{p}(Ĉ′, ρ′) = (Ĉ, ρ̂).

Proof. We can immediately see that F_{p}(G_{p}(Ĉ′, ρ′)) = (Ĉ′, ρ′) and that G_{p}(F_{p}(Ĉ, ρ̂)) ⊑ (Ĉ, ρ̂). Therefore, G_{p} and F_{p} form an embedding/projection pair.

Since (Ĉ, ρ̂) is the least solution, then (Ĉ, ρ̂) ⊑ G_{p}(Ĉ′, ρ′). Using the monotonicity of G_{p}, we obtain that F_{p}(Ĉ, ρ̂) ⊑ F_{p}(G_{p}(Ĉ′, ρ′)) = (Ĉ′, ρ′). Since F_{p}(Ĉ, ρ̂) is a solution and (Ĉ′, ρ′) is the least solution, we obtain that F_{p}(Ĉ, ρ̂) = (Ĉ′, ρ′) and then that G_{p}(Ĉ′, ρ′) = (Ĉ, ρ̂).

4.2 The CPS transformation of flow information and administrative reductions

Lemma 4.3 says that the least analysis after a linear β-reduction is a restriction of the least analysis of the initial term. From this, we can infer that any linear β-reduction does not alter the results of the CFA. We use this result to show that administrative reductions after Plotkin’s CPS transformation do not change the result of the flow analysis.

Theorem 4.4. Let p be a program, p_{1} be its CPS counterpart without administrative reductions, and p_{2} be its CPS counterpart after administrative reduction. Let (Ĉ_{1}, ρ̂_{1}) be the least solution of the analysis of p_{1}. The least solution (Ĉ_{2}, ρ̂_{2}) of the analysis of p_{2} can be obtained in linear time from (Ĉ_{1}, ρ̂_{1}), by restricting (Ĉ_{1}, ρ̂_{1}) to the program points preserved by the administrative reductions.

Proof. All administrative reductions are linear, and furthermore, administrative reduction is known to terminate [4]. We apply Lemma 4.3.

Corollary 4.5. Let p be a program, p_{1} be its CPS counterpart without administrative reductions, and p_{2} be its CPS counterpart after administrative reduction. Let (Ĉ, ρ̂) be the least solution of the analysis of p. The least solution (Ĉ_{2}, ρ̂_{2}) of the analysis of p_{2} can be obtained in linear time from (Ĉ, ρ̂).

Proof. We compose the construction given by Theorem 4.4 with Palsberg and Wand’s CPS transformation of flow information [11], which also works in linear time.

5 Related work

Our key observation is that linear β-reduction preserves leastness. This property is a corollary of Henglein’s subject invariance property of linear β-reductions for monomorphic program analyses [6–8]. Non-linear β-reductions, while they do preserve correctness of an analysis [17], are known not to preserve leastness.

6 Conclusion and issues

We have shown how to complement Palsberg and Wand’s CPS transformation of flow information with administrative reductions, while preserving its linear-time complexity. Our extension hinges on the linearity of administrative redexes.

Let us now show how to integrate administrative reductions in Palsberg and Wand’s CPS transformation, therefore making it operate in one pass, still in linear time. As shown in “Representing Control” [4], at CPS-transformation time, one can segregate the administrative lambdas and applications and the residual ones. (The residual lambdas and applications are the ones preserved by the administrative reductions.) Therefore, in Palsberg and Wand’s CPS transformation of flow information, we can segregate the labels of the administrative lambdas and applications and the labels of the residual ones as well. In practice, the solution after administrative reduction is thus obtained simply by restricting Palsberg and Wand’s solution to the residual labels. In the overall process of (1) CPS transformation and (2) administrative reduction, the administrative labels are used transitorily, just as in the one-pass CPS transformation, which is conceptually fitting.

References

[1] Daniel Damian. On Static and Dynamic Control-Flow Information in Program Analysis and Transformation. PhD thesis, BRICS PhD School, University of Aarhus, Aarhus, Denmark, July 2001. BRICS DS-01-5.

[2] Daniel Damian and Olivier Danvy. Syntactic accidents in program analysis: On the impact of the CPS transformation. In Philip Wadler, editor, Proceedings of the 2000 ACM SIGPLAN International Conference on Functional Programming, SIGPLAN Notices, Vol. 35, No. 9, pages 209–220, Montréal, Canada, September 2000. ACM Press. Extended version to appear in the Journal of Functional Programming.

[3] Daniel Damian and Olivier Danvy. Syntactic accidents in program analysis: On the impact of the CPS transformation. Journal of Functional Programming, 2002. To appear. Extended version available as the technical report BRICS-RS-01-54.

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

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

[6] Fritz Henglein. Dynamic typing: Syntax and proof theory. Science of Computer Programming, 22(3):197–230, 1994.

[7] Fritz Henglein and Harry Mairson. The complexity of type inference for higherorder typed lambda calculi. In Robert (Corky) Cartwright, editor, Proceedings of the Eighteenth Annual ACM Symposium on Principles of Programming Languages, pages 119–130, Orlando, Florida, January 1991. ACM Press.

[8] Fritz Henglein and Harry Mairson. The complexity of type inference for higherorder typed lambda calculi. Journal of Functional Programming, 4(4):435–477, 1994.

[9] Albert R. Meyer and Mitchell Wand. Continuation semantics in typed lambdacalculi (summary). In Rohit Parikh, editor, Logics of Programs – Proceedings, number 193 in Lecture Notes in Computer Science, pages 219–224, Brooklyn, New York, June 1985. Springer-Verlag.

[10] Flemming Nielson, Hanne Riis Nielson, and Chris Hankin. Principles of Program Analysis. Springer Verlag, 1999.

[11] Jens Palsberg and Mitchell Wand. CPS transformation of flow information. Journal of Functional Programming, 2002. To appear.

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

[13] John C. Reynolds. The discoveries of continuations. Lisp and Symbolic Computation, 6(3/4):233–247, 1993.

[14] Amr Sabry and Philip Wadler. A reflection on call-by-value. ACM Transactions on Programming Languages and Systems, 19(6):916–941, 1997.

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

[16] Mitchell Wand. Embedding type structure in semantics. In Mary S. Van Deusen and Zvi Galil, editors, Proceedings of the Twelfth Annual ACM Symposium on Principles of Programming Languages, pages 1–6, New Orleans, Louisiana, January 1985. ACM Press.

[17] Mitchell Wand and Galen B. Williamson. A modular, extensible proof method for small-step flow analyses. In Daniel Le Métayer, editor, Programming Languages and Systems, 11th European Symposium on Programming, ESOP 2002, number 2305 in Lecture Notes in Computer Science, pages 213–227, Grenoble, France, April 2001. Springer-Verlag.

Recent BRICS Report Series Publications

RS-02-36 Daniel Damian and Olivier Danvy. CPS Transformation of Flow Information, Part II: Administrative Reductions. August 2002. 9 pp. To appear in the Journal of Functional Programming. This report supersedes the earlier BRICS report RS-01-40.

RS-02-35 Patricia Bouyer. Timed Automata May Cause Some Troubles. August 2002. 44 pp.

RS-02-34 Morten Rhiger. A Foundation for Embedded Languages. August 2002. 29 pp.

RS-02-33 Vincent Balat and Olivier Danvy. Memoization in Type-Directed Partial Evaluation. July 2002. 18 pp. To appear in Batory and Consel, editors, ACM SIGPLAN/SIGSOFT Conference on Generative Programming and Component Engineering, GPCE ’02 Proceedings, LNCS, 2002.

RS-02-32 Mads Sig Ager, Olivier Danvy, and Henning Korsholm Rohde. On Obtaining Knuth, Morris, and Pratt’s String Matcher by Partial Evaluation. July 2002. 43 pp. To appear in Chin, editor, ACM SIGPLAN ASIAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, ASIA-PEPM ’02 Proceedings, 2002.

RS-02-31 Ulrich Kohlenbach and Paulo B. Oliva. Proof Mining: A Systematic Way of Analysing Proofs in Mathematics. June 2002. 47 pp.

RS-02-30 Olivier Danvy and Ulrik P. Schultz. Lambda-Lifting in Quadratic Time. June 2002.

RS-02-29 Christian N. S. Pedersen and Tejs Scharling. Comparative Methods for Gene Structure Prediction in Homologous Sequences. June 2002. 20 pp.

RS-02-28 Ulrich Kohlenbach and Laurenţiu Leuştean. Mann Iterates of Directionally Nonexpansive Mappings in Hyperbolic Spaces. June 2002. 33 pp.

RS-02-27 Anna Östlin and Rasmus Pagh. Simulating Uniform Hashing in Constant Time and Optimal Space. 2002. 11 pp.

RS-02-26 Margarita Korovina. Fixed Points on Abstract Structures without the Equality Test. June 2002.