BRICS

Basic Research in Computer Science

Program Extraction from Proofs of Weak Head Normalization

Ma�gorzata Biernacka Olivier Danvy Kristian Støvring BRICS Report Series RS-05-12 ISSN 0909-0878 April 2005 BRICS RS-05-12 Biernacka et al.: Program Extraction from Proofs of Weak Head Normalization Copyright \begin{matrix}c \\ ◯ \end{matrix} 2005, Ma�gorzata Biernacka & Olivier Danvy &

Kristian Støvring. 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/05/12/

                        MFPS XX1 Preliminary Version

Program extraction from proofs of weak head normalization

Małgorzata Biernacka, Olivier Danvy, and Kristian Støvring

BRICS^{1}

Department of Computer Science, University of Aarhus IT-parken, Aabogade 34, 8200 Aarhus N, Denmark

Abstract

We formalize two proofs of weak head normalization for the simply typed lambdacalculus in first-order minimal logic: one for normal-order reduction, and one for applicative-order reduction in the object language. Subsequently we use Kreisel’s modified realizability to extract evaluation algorithms from the proofs, following Berger; the proofs are based on Tait-style reducibility predicates, and hence the extracted algorithms are instances of (weak head) normalization by evaluation, as already identified by Coquand and Dybjer.

Key words: program extraction, normalization by evaluation, weak head normalization.

1 Introduction and related work

In the early nineties, Berger and Schwichtenberg introduced normalization by evaluation in a proof-theoretic setting [5]. Berger then substantiated their normalization function by extracting it from a proof of strong normalization [2], using Kreisel’s modified realizability interpretation [11]. In their own study of what also turned out to be normalization by evaluation [7,8], Coquand and Dybjer constructed normalization functions interpreting source terms in so-called glueing models. They also outlined a process of “program extraction” with which their normalization algorithms can be obtained from simple instances of a normalization proof due to Martin-Löf, and noticed the connection with Berger’s work. In this article, we use part of Berger’s framework to formalize some of the relationship identified by Coquand and Dybjer between glueing models and Tait-style proofs as used by Martin-Löf. We consider two intuitionistic proofs of weak head normalization for the simply typed λ-calculus: A normal-order proof essentially due to Martin-Löf, and an applicative-order counterpart due to Hofmann [12, page 152].

1

Basic Research in Computer Science (www.brics.dk),

funded by the Danish National Research Foundation.

This is a preliminary version. The final version will be published in Electronic Notes in Theoretical Computer Science

                       URL: www.elsevier.nl/locate/entcs

Biernacka, Danvy, and Støvring

Our results can be described informally as follows: Applying modified realizability to the definition of the Tait-style reducibility predicate gives the definition of a glueing model. Applying modified realizability to the proof of normalization of a particular simply typed term t gives a λ-term denoting the interpretation of t in this glueing model.

The program extraction we perform can be intuitively explained as a “program optimization” [7]: Martin-Löf’s normalization proof is formalized in an intuitionistic meta-language, and such a proof can informally be regarded as a function returning the normal form, together with a proof that this result actually is a normal form [7,9]. To go from such a normalization proof to a function returning only the normal form, one can then remove the redundant parts representing the axioms for convertibility, and simplify the types accordingly [7]. Berger’s use of the modified realizability interpretation works like that (in the setting of first-order logic): the axioms for convertibility can be stated as Harrop formulas, and subproofs which are proofs of Harrop formulas disappear during the extraction.

Coquand and Dybjer’s weak normalization function for the λ-calculus can be perceived as an optimized version of the program we extract in the applicative-order case. This is not surprising, since our focus here is on formalizing the proofs and considering two different evaluation strategies in the object language rather than optimizing the extracted programs. In doing so, we identify certain technical difficulties arising with the applicative-order case, and we adjust the extraction method to solve them. In his recent work [3], Berger has proposed a similar refinement as part of a bigger framework, the Uniform Heyting Arithmetic.

Our account has the following limitations:

• Like Berger, we only partially formalize the normalization proof. Since a part of the proof is performed at the meta-level, we cannot formally extract a normalization function, but only a λ-term denoting the glueing interpretation of t for every particular term t.

• For simplicity, we only consider normalization of closed terms. With this restriction, we do not need to formalize renaming of bound variables.

• We only treat the case of the simply typed λ-calculus with one uninterpreted base type, whereas Coquand and Dybjer consider a variety of more advanced examples.

In the remainder of this article, we first review the modified realizability interpretation (Section 2); we then specify the problem of weak head normalization for the λ-calculus and we extract a call-by-name λ-interpreter and then a call-by-value λ-interpreter (Section 3). ML implementations of the extracted normalization programs are presented in Appendix A.

2 Preliminaries

We begin by reviewing the techniques used by Berger to extract normalization functions from proofs [2]. The key concept is Kreisel’s modified realizability proof interpretation [11]. Our presentation is based on Berger’s article [2] and Troelstra’s treatise [14].

2.1 First-order minimal logic

We formalize the normalization proofs in a first-order logic M_{1}. The language of M_{1} is that of many-sorted first-order minimal logic with conjunction, defined in a standard way. Specifically, such a language is given by:

• Sorts ι, ι_{1}, ι_{2}, …

• Constants c^{ι}, function symbols f^{ι_{1}×...×ι_{n}→ι}.

• Predicate symbols P^{ι_{1}×...×ι_{n}}.

(We will see that the sorts of M_{1} are the base types of the extracted programs.) The terms and formulas of M_{1} are:

Terms  t^{ι} := x^{ι} | c^{ι} | f^{ι_{1}×...×ι_{n}→ι}(t_{1}^{ι_{1}}, …, t_{n}^{ι_{n}})
Formulas  ϕ, ψ := P^{ι_{1}×...×ι_{n}}(t_{1}^{ι_{1}}, …, t_{n}^{ι_{n}}) | ϕ ∧ ψ | ϕ → ψ | ∀x^{ι}. ϕ | ∃x^{ι}. ϕ

A natural deduction proof system of M_{1} is shown in Figure 1. Instead of presenting the proof rules graphically, we directly define a proof of a formula ϕ to be a dependently typed λ-term d^{ϕ}. In the definition, FV(ϕ) denotes the set of free variables in the formula ϕ, while FA(d) denotes the set of free assumptions in the proof d. Only the interesting defining cases of FA(d) are shown.

We will also use the notation u_{1} : ψ_{1}, …, u_{n} : ψ_{n} ⊢_{M_{1}} d : ϕ to mean that d^{ϕ} is an M_{1}-proof of ϕ with free assumptions contained in the set {u_{1}^{ψ_{1}}, …, u_{n}^{ψ_{n}}}.

2.2 Modified realizability

In the presentation we use one of Troelstra’s variants of modified realizability [14, p. 218].

The programs extracted from proofs are terms of the simply typed λ-calculus with product and unit types, and with the sorts of M_{1} as base types:

Types  σ := 1 | ι_{1} | ι_{2} | … | σ_{1} → σ_{2} | σ_{1} × σ_{2}
Terms  t := x^{σ} | t_{0} t_{1} | λx^{σ}.t | fst t | snd t | (t_{1}, t_{2}) | ∗ | c | f(t_{1}, …, t_{n})

Note that the language of λ-terms includes the constants and function symbols of M_{1}. Moreover, meta-variables ranging over λ-terms are denoted with the Roman font (t), and thus differ from the notation for logical terms in M_{1} (t).

In the following, by a “program” we mean a simply typed λ-term as just defined. Only in Appendix A are actual programming language implementations considered [6].

Definition 2.1 [Program extraction] Given an M_{1}-proof d of ϕ, we define a type τ(d) and a λ-term [[d]] of type τ(d) as follows:

(ass.) u^{ϕ}
(→^{+}) (λu^{ϕ}.d^{ψ})^{ϕ→ψ}
(→^{−}) (d^{ϕ→ψ} e^{ϕ})^{ψ}
(∧^{+}) (d^{ϕ}, e^{ψ})^{ϕ∧ψ}
(∧_{1}^{−}) (fst d^{ϕ∧ψ})^{ϕ}
(∧_{2}^{−}) (snd d^{ϕ∧ψ})^{ψ}
(∀^{+}) (λx^{ι}.d^{ϕ})^{∀x^{ι}. ϕ}

(provided x^{ι} ∉ FV(ψ) for every u^{ψ} ∈ FA(d))

(∀^{−}) (d^{∀x^{ι}. ϕ} t^{ι})^{ϕ [t/x]}
(∃^{+}) ⟨t, d^{ϕ [t/x]}⟩^{∃x. ϕ}
(∃^{−}) [e^{∃x. ϕ}, u^{ϕ}.d^{ψ}]^{ψ}

(provided x ∉ FV(ψ),

and x ∉ FV(χ) for every v^{χ} ∈ FA(d) \ {u^{ϕ}})

where FA(u^{ϕ}) = {u^{ϕ}} FA((λu^{ϕ}.d^{ψ})^{ϕ→ψ}) = FA(d^{ψ}) \ {u^{ϕ}} FA([e^{∃x. ϕ}, u^{ϕ}.d^{ψ}]^{ψ}) = FA(e^{∃x. ϕ}) ∪ (FA(d^{ψ}) \ {u^{ϕ}}) etc.

Fig. 1. The proof system M_{1}

\begin{aligned}τ(P(t_{1}, …, t_{n})) & := & 1 \\ τ(ϕ ∧ ψ) & := & τ(ϕ) × τ(ψ) \\ τ(ϕ → ψ) & := & τ(ϕ) → τ(ψ) \\ τ(∀x^{ι}. ϕ) & := & ι → τ(ϕ) \\ τ(∃x^{ι}. ϕ) & := & ι × τ(ϕ) \end{aligned} [[u^{ϕ}]]  := x_{u}^{τ(ϕ)}

[[λu^{ϕ}.d^{ψ}]]  := λx_{u}^{τ(ϕ)}.[[d]]
[[d^{ϕ→ψ} e^{ϕ}]]  := [[d]] [[e]]
[[(d^{ϕ}, e^{ψ})]]  := ([[d]], [[e]])
[[fst d^{ϕ∧ψ}]]  := fst [[d]]
[[snd d^{ϕ∧ψ}]]  := snd [[d]]
[[λx^{ι}.d^{ϕ}]]  := λx^{ι}.[[d]]
[[d^{∀x^{ι}. ϕ} t^{ι}]]  := [[d]] t
[[⟨t, d^{ϕ [t/x]}⟩]] := (t, [[d]])
[[[e^{∃x. ϕ}, u^{ϕ}.d^{ψ}]]] := [[d]][fst [[e]]/x, snd [[e]]/x_{u}]

Subsequently, we simplify the extracted terms using the isomorphisms A × 1 ≅ A, 1 × B ≅ B, A → 1 ≅ 1, and 1 → B ≅ B.^{2} This means that the type τ(ϕ) of an extracted term will either be 1 or not contain 1 at all. The first case happens exactly

2 In the original version of modified realizability [11], as well as in newer variants [4], this “optimization” is built-in. We use the simpler version for presentational purposes.

when ϕ is a Harrop formula—we then informally say that ϕ “has no computational content.”

2.2.1 Soundness of the extraction

We now briefly consider in what sense a λ-term extracted from a proof of ϕ “realizes” ϕ. The notion of realizability is formalized in a finite-type extension M_{1}^{−}(λ) of M_{1} [2]. The point is that every extracted term [[d]] is a term of M_{1}^{−}(λ).

Definition 2.2 [Modified realizability] By induction on the M_{1}-formula ϕ we define an M_{1}^{−}(λ)-formula t^{τ(ϕ)} mr ϕ as follows:

t^{1} mr P(t_{1}, …, t_{n}) := P(t_{1}, …, t_{n})
t^{σ_{1}×σ_{2}} mr ϕ ∧ ψ  := (fst t) mr ϕ ∧ (snd t) mr ψ
t^{σ_{1}→σ_{2}} mr ϕ → ψ  := ∀y^{σ_{1}}. (y mr ϕ → t y mr ψ)
t^{ι→σ} mr ∀z^{ι}. ϕ(z)  := ∀z^{ι}. t z mr ϕ(z)
t^{ι×σ} mr ∃z^{ι}. ϕ(z)  := (snd t) mr ϕ(fst t)

Given an M_{1}-proof d of ϕ, the goal is therefore to give an M_{1}^{−}(λ)-proof of [[d]] mr ϕ. It turns out that the proof d is allowed to contain free assumptions of Harrop formulas.

Theorem 2.3 (Soundness of modified realizability) Let ψ_{1}, …, ψ_{n} be Harrop formulas. If u_{1} : ψ_{1}, …, u_{n} : ψ_{n} ⊢_{M_{1}} d : ϕ, then ψ_{1}, …, ψ_{n} ⊢_{M_{1}^{−}(λ)} [[d]] mr ϕ.

Proof. Standard [2,14]. □

As an example, suppose that d is a M_{1}-proof of ∀x. ∃y. P(x, y) containing only Harrop formulas as free assumptions. Then Theorem 2.3 gives an M_{1}^{−}(λ)-proof of ∀x. P(x, fst([[d]] x)) from the same free assumptions. In this way, free Harrop assumptions can be thought of as “axioms” with no effect on the extracted program.

2.2.2 Eliminating computationally redundant variables

The extraction procedure can be refined in order to keep the resulting programs simple. We first present a refinement due to Berger [2] which allows computationally redundant universal variables to be eliminated from the extracted program. To this end, we add a new kind of formulas of the form {∀x}. ϕ with the following introduction and elimination rules:

(∀^{+}) ({λx^{ι}}.d^{ϕ})^{{∀x^{ι}}. ϕ}
(provided x^{ι} ∉ FV(ψ) for every u^{ψ} ∈ FA(d)) and x ∉ CV(d))
(∀^{−}) (d^{{∀x^{ι}}. ϕ} {t^{ι}})^{ϕ [t/x]},

where the set of computationally relevant variables CV(d) is defined as the set of all variables occurring free in a witness for an existential quantifier, or in any term instantiating a universal quantifier in d. A universally quantified variable is called redundant if it is not computationally relevant.

The type of realizers for the new formulas simply ignores the redundant variable: τ({∀x}. ϕ) := τ(ϕ). The corresponding clause for modified realizability is t mr {∀x}. ϕ := ∀x. t mr ϕ (with x ∉ FV(t)). As desired, the extracted program does not contain the redundant variable:

\begin{aligned}[[\{λx\}.d]] & := & [[d]] \\ [[d \{t\}]] & := & [[d]] \end{aligned}

The proof of soundness of modified realizability can be extended to handle this case [2].

The second refinement allows us to choose which of the existential quantifiers in a formula we want to have witnesses of. However, we postpone the description of this extension until Section 3.3, where it will be essential that not all of the existential quantifiers are realized.

3 Weak head normalization

We now specify the problem of weak head normalization for the λ-calculus. In the presentation, we assume that all terms are well-typed, but for clarity we omit all typing annotations. We consider only closed terms.

By normalization we understand the process of reducing a term to a normal form, where the basic reduction step is β-reduction [1]:

(λx.t) s → t [s/x].

The compatible closure of β-reduction yields the one-step reduction relation. Weak head normalization is a restricted form of normalization producing terms

in weak head normal form, which—for closed terms—stops at a λ-abstraction, without normalizing its body. Therefore any λ-abstraction is in weak head normal form.

We consider two deterministic restrictions of the one-step reduction that lead to weak head normal forms: the normal-order and applicative-order reduction strategies. Since weak head normalization is closely related to evaluation in the λ-calculus regarded as a programming language, where computations are not performed under λ-abstractions, we also refer to the above reduction strategies as the call-by-name and call-by-value evaluation strategies, respectively [13].

Definition 3.1 [Normal-order reduction] The normal-order reduction strategy is obtained from one-step reduction by restricting it to the following rules:

\begin{matrix}(β) & (λx.r) s → r [s/x] \\ (ν) & \frac{r → r′}{r s → r′ s} \end{matrix}

Definition 3.2 [Applicative-order reduction] The (left-to-right) applicative-order reduction strategy is obtained from one-step reduction by restricting it to the following rules:

(β_{v}) (λx.r) s → r [s/x] if s is a value
(ν)  \frac{r → r′}{r s → r′ s}
(μ_{v})  \frac{s → s′}{r s → r s′}  if r is a value

Values are λ-abstractions.

These specifications of evaluation strategies can be axiomatized directly in the logic M_{1} using only Harrop formulas, as will be shown in the following sections.

The theorem we want to prove can be stated informally as follows:

Theorem 3.3 (Weak head normalization) The process of reducing a closed well-typed λ-term according to either of the above strategies terminates with a (weak head) normal form.

The proof proceeds by first defining a suitable logical relation on well-typed closed terms that implies the desired property. Next we show that every well-typed term satisfies this relation. Obviously, the exact shape of the proof relies on the chosen reduction strategy (normal-order or applicative-order), and consequently the extracted program produces the result according to the corresponding strategy in the object language (call by name or call by value).

In the rest of the section we first formalize this theorem for the two evaluation strategies, and then we use modified realizability to extract the underlying programs. For the case of call-by-name evaluation this is a straightforward exercise, whereas in the call-by-value case we need to refine the extraction procedure further. Our development in this section formalizes and extends the proof of normalization for call-by-value evaluation presented in Pierce’s book [12, pp. 149-152].

3.1 The object language

We consider an explicitly typed version of the simply typed λ-calculus with variables contained in a countable set V = x_{1}^{T_{1}}, x_{2}^{T_{2}}, … (infinitely many of each type). This language is now encoded in a first-order minimal logic. The variables are used to index the sorts and constants of the logic, which is given by the following:

• Sorts: For every type T and finite set of variables X, we have the sort Λ_{T}^{X} of object-level λ-terms of type T containing exactly free variables X.

• Constants: The λ-term constructors are:

VAR_{x} : Λ_{T}^{{x}}  (for each variable x^{T})
LAM_{x,T_{1},T_{2},X} : Λ_{T_{2}}^{X} → Λ_{T_{1}→T_{2}}^{X\{x}}  (where x has type T_{1})
APP_{T_{1},T_{2},X,Y} : Λ_{T_{1}→T_{2}}^{X} → Λ_{T_{1}}^{Y} → Λ_{T_{2}}^{X∪Y}

• Predicate symbols: the set of predicate symbols differs for call-by-name and callby-value evaluation, and we specify each of them in Section 3.2 and Section 3.3, respectively.

Notation. For the sake of presentation, we use a number of notational abbreviations when constructing object terms, e.g., we omit type annotations from λ-term constructors—in most cases they can be inferred from the context; we use the “uncurried” versions of the term constructors; we also write LAM x_{i}. t instead of LAM_{x_{i},T_{1},T_{2},X}(t), and VAR x_{i} instead of VAR_{x_{i}}.

We abbreviate sorts of closed terms Λ_{T}^{∅} as Λ_{T}. In the formulas used in the rest of this article, we only quantify over sorts of closed terms.

We treat substitution in λ-terms at the meta level. For a variable x_{i}^{T_{1}} and logical terms s^{Λ_{T_{1}}} and t^{Λ_{T_{2}}} , we define t [s/VAR x_{i}] as t with every subterm VAR x_{i} not in scope of a LAM_{x_{i}} replaced by s. As Λ_{T_{1}} is a sort of closed λ-terms, free objectlevel variables are never captured as a result of this form of substitution. For this definition of t [s/VAR x_{i}] to faithfully encode substitution, we further require that all free logical variables in t range over sorts of closed object-level terms. Thus the formal definition of substitution is as follows:

Definition 3.4 Let x_{i}^{T_{1}} be a variable, and let s^{Λ_{T_{1}}^{∅}} and t^{Λ_{T_{2}}^{X}} be logical terms such that all free logical variables in t belong to (possibly different) sorts Λ_{T}^{∅} of closed object-level terms. We define the term t [s/VAR x_{i}] of sort Λ_{T_{2}}^{X\{x_{i}}} inductively:

y^{Λ_{T}^{∅}} [s/VAR x_{i}] = y  (where y is a logical variable)
VAR x_{i} [s/VAR x_{i}] = s
VAR x_{j} [s/VAR x_{i}] = VAR x_{j}  (j ≠ i)
APP(t_{1}, t_{2}) [s/VAR x_{i}] = APP(t_{1} [s/VAR x_{i}], t_{2} [s/VAR x_{i}])
(LAM_{x_{i},X} t_{1}) [s/VAR x_{i}] = LAM_{x_{i},X} t_{1}
(LAM_{x_{j},X} t_{1}) [s/VAR x_{i}] = LAM_{x_{j},X\{x_{i}}} (t_{1} [s/VAR x_{i}])  (j ≠ i)

3.2 Call-by-name evaluation

First, we give an axiomatization of call-by-name evaluation in the λ-calculus. We use two primitive predicates: Ev(t, s), understood as “t evaluates to s,” and Rd(t, s), understood as “t reduces to s in one step.” The process of call-by-name evaluation is defined through the following axioms:

(A_{1}) {∀s}. Rd(APP(LAM x_{i}. t, s), t [s/VAR x_{i}])
(A_{2}) {∀rst}. Rd(r, s) → Rd(APP(r, t), APP(s, t))
(A_{3}) {∀rst}. Rd(r, s) → Ev(s, t) → Ev(r, t)
(A_{4}) Ev(t, t) for all terms t = LAM x_{i}. s

The first and the last axioms are schematic in the logical term t whose free logical variables must range over sorts of closed object-level terms. As explained above, this restriction is necessary for the meta-level definition of substitution to be correct.

The axioms formally capture the idea that (call-by-name) evaluation is the reflexive, transitive closure of (normal-order) one-step reduction as defined above. The notion of reduction is β-reduction (axiom (A_{1})); it can be applied to left-most redexes (axiom (A_{2})) yielding a one-step reduction relation. The evaluation stops when a λ-abstraction is reached (the family of axioms (A_{4})); otherwise it is defined as the transitive closure of one-step reduction (axiom (A_{3})).

In the proofs, we will use free assumption variables A_{1}, A_{2}, A_{3}, A_{4} corresponding to the respective axioms above. Since all the axioms are Harrop formulas, these free variables will not occur in the extracted programs.

3.2.1 Formalizing the proof

The logical relation used in the proof is defined as follows:

R_{b}(t)  := ∃v.Ev(t, v)
R_{T_{1}→T_{2}}(t) := ∃v.Ev(t, v) ∧ ∀s. R_{T_{1}}(s) → R_{T_{2}}(APP(t, s))

A term of an arrow type satisfying the relation R_{T} is not only required to evaluate to a value (or “halt”, in Pierce’s terms [12, p. 150]), but it should also halt when applied to another halting term. This stronger condition allows to prove the desired theorem for both call-by-value and call-by-name evaluation strategies. If we are only interested in evaluation at base types, a weaker condition is actually enough to prove the normalization theorem for call-by-name evaluation (see Section 3.4), but for the call-by-value case we still need this stronger definition.

We immediately see that every term satisfying the relation R_{T} evaluates to a value:

Lemma 3.5 {∀t}. R_{T} (t) → ∃v.Ev(t, v).

Proof. By induction on types at the meta level. The corresponding proof terms are:

p_{1}^{b} = {λt}.λu^{R_{b}(t)}.u
p_{1}^{T_{1}→T_{2}} = {λt}.λu^{R_{T_{1}→T_{2}}(t)}.fst u
□

To prove the main lemma, we need the following property.

Lemma 3.6 {∀rs}. Rd(r, s) → R_{T} (s) → R_{T} (r).

Proof. By induction on types at the meta level.

Case b. Assume Rd(r, s) and R_{b}(s). By Lemma 3.5, we obtain ∃v.Ev(s, v) from R_{b}(s). Then using axiom (A_{3}) we deduce ∃v.Ev(r, v).

The proof term corresponding to this case is as follows:

p_{2}^{b} = {λrs}.λu^{Rd(r,s)}v^{R_{b}(s)}.[p_{1}^{b} v, w^{Ev(s,v′)}.⟨v′, A_{3} {rsv′}u w ⟩]

Case T_{1} → T_{2}. Assume Rd(r, s) and R_{T_{1}→T_{2}}(s). We need to prove ∃v.Ev(r, v) and ∀t. R_{T_{1}}(t) → R_{T_{2}}(APP(r, t)). The first fact is proved analogously to the base case. For the second, assume that R_{T_{1}}(t) holds for some t. By axiom (A_{2}) we obtain Rd(APP(r, t), APP(s, t)). Next, unwinding the definition of R_{T_{1}→T_{2}}(s) yields R_{T_{2}}(APP(s, t)). Hence, by induction hypothesis we conclude that R_{T_{2}}(APP(r, t)). Here is the corresponding proof term:

p_{2}^{T_{1}→T_{2}} = {λrs}.λu^{Rd(r,s)}v^{R_{T_{1}→T_{2}}(s)}.(p_{2,1}^{T_{1}→T_{2}}, p_{2,2}^{T_{1}→T_{2}})

where

p_{2,1}^{T_{1}→T_{2}} = [p_{1}^{T_{1}→T_{2}} v, w^{Ev(s,v′)}.⟨v′, A_{3} {rsv′} u w⟩]
p_{2,2}^{T_{1}→T_{2}} = λt^{Λ_{T_{1}}} z^{R_{T_{1}}(t)}.p_{2}^{T_{2}} {APP(r, t)APP(s, t)} (A_{2} {rst} u) (snd v s z)

□

Lemma 3.7 For any term t of type T, with FV(t) = {x_{1}, …, x_{n}}, and for any n-tuple of closed terms r⃗ = r_{1}, …, r_{n} of types T_{i} such that R_{T_{i}}(r_{i}) holds for all 1 ≤ i ≤ n, we have

R_{T} (t [r⃗/x⃗]).

(We use the abbreviation t [r⃗/x⃗] for t [r_{1}/VAR x_{1}] ⋯ [r_{n}/VAR x_{n}].)

Proof. By induction on the typing derivation (or, on the structure of t, parameterized by the set of free variables). The formula to prove is

∀r⃗. (R_{T_{1}}(r_{1}) ∧ … ∧ R_{T_{n}}(r_{n})) → R_{T} (t [r⃗/x⃗]).

Case t = VAR x_{i}^{T} . Obvious. p_{3}^{VAR x_{i},x⃗} = λr⃗u⃗.u_{i}.

Case t = APP(s_{1}^{T_{1}→T} , s_{2}^{T_{1}}). We apply the induction hypothesis to both subterms to obtain R_{T_{1}→T} (s_{1} [r⃗/x⃗]) and R_{T_{1}}(s_{2} [r⃗/x⃗]). Unwinding the definition of R_{T_{1}→T} (s_{1} [r⃗/x⃗]) then yields R_{T} (APP(s_{1}, s_{2}) [r⃗/x⃗]) (using APP(s_{1} [r⃗/x⃗], s_{2} [r⃗/x⃗]) = APP(s_{1}, s_{2}) [r⃗/x⃗]).

p_{3}^{APP(s_{1},s_{2}),x⃗} = λr⃗u⃗.snd(p_{3}^{s_{1},x⃗} r⃗u⃗) (s_{2} [r⃗/x⃗]) (p_{3}^{s_{2},x⃗} r⃗u⃗).

Case t = LAM x_{n+1}^{T_{1}}. r^{T_{2}}(T = T_{1} → T_{2}). We need to show that ∃v.Ev(t [r⃗/x⃗], v) and ∀s. R_{T_{1}}(s) → R_{T_{2}}(APP(t [r⃗/x⃗], s)). The first fact follows from (an instance of) the axiom (A_{4}), since (LAM x_{n+1}. r) [r⃗/x⃗] is a λ-abstraction. For the second, assume that R_{T_{1}}(s) holds for some s. By induction hypothesis, R_{T_{2}}(r [r⃗/x⃗] [s/x_{n+1}]) holds. We now obtain R_{T_{2}}(APP(LAM x_{n+1}. r [r⃗/x⃗], s)) using axiom (A_{1}) and Lemma 3.6, which concludes the proof. The corresponding proof term reads as follows:

p_{3}^{LAM x_{n+1}. r,x⃗} = λr⃗u⃗.(p_{3,1}, p_{3,2})

where

p_{3,1} = ⟨(LAM x_{n+1}. r) [r⃗/x⃗], A_{4}⟩

p_{3,2} = λs^{Λ_{T_{1}}} v^{R_{T_{1}}(s)}.p_{2}^{T_{2}} {t_{1}t_{2}} (A_{1} {s}) p_{3}^{r,x⃗x_{n+1}} (r⃗s) (u⃗v)

with

t_{1} = APP(LAM x_{n+1}. r [r⃗/x⃗], s)

t_{2} = r [r⃗/x⃗] [s/VAR x_{n+1}]

□

The normalization theorem can now be stated formally as follows.

Theorem 3.8 For any closed term t of type T, ∃v.Ev(t, v) holds.

Proof. By Lemma 3.7, R_{T} (t) holds. Hence, by Lemma 3.5, ∃v.Ev(t, v) holds.

p = p_{1}^{T} (p_{3}^{t} ε ε),

where ε denotes the empty tuple. □

3.2.2 Extracted program

Since the induction on the structure of terms in the proof of Lemma 3.7 is done at the meta level, from the proof of Theorem 3.8 we do not obtain one extracted program of type Λ_{T} → Λ_{T} realizing the formula ∀t^{Λ_{T}} . ∃v^{Λ_{T}} . Ev(t, v), but rather— for each term t^{Λ_{T}} —we extract a program ‘computing’ a term v such that Ev(t, v) is provable in M_{1}^{−}(λ) [2].

We first consider the types τ(R_{T} (t)) of programs extracted from Lemma 3.7 (for specific terms t^{Λ_{T}}.) We see that the types τ(R_{T} (t)) are independent of t, and that they can be characterized inductively like this:

τ(R_{b})  := Λ_{b}
τ(R_{T_{1}→T_{2}}) := Λ_{T_{1}→T_{2}} × (Λ_{T_{1}} → τ(R_{T_{1}}) → τ(R_{T_{2}}))

This defines the semantic domains of a glueing model similar to the ones considered by Coquand and Dybjer (relative to any particular model of M_{1}^{−}(λ)).

The terms extracted from Lemma 3.7 can be inductively described as follows (they are parameterized by a tuple of free variables x⃗):

eval_{VAR x_{i},x⃗}  = λt⃗u⃗.u_{i}
eval_{APP(r,s),x⃗} = λt⃗u⃗.snd(eval_{r,x⃗} t⃗u⃗) (s [t⃗/x⃗]) (eval_{s,x⃗} t⃗u⃗)
eval_{LAM x_{n+1}. t,x⃗} = λt⃗u⃗.(LAM x_{n+1}. t [t⃗/x⃗], λsv.[[p_{2}^{T}]] (eval_{t,x⃗x_{n+1}} (t⃗s)(u⃗v)))

with

[[p_{2}^{b}]]  = λu.u
[[p_{2}^{T_{1}→T_{2}}]]  = λx.(fst x, λsv.[[p_{2}^{T_{2}}]] ((snd x) s v))

(Note that [[p_{2}^{T}]] is βη×-equivalent to the identity function.) For every closed term t^{Λ_{T}}, eval_{t,ε} denotes the glueing model interpretation of the object-level term denoted by t^{Λ_{T}}.

From Lemma 3.5 we obtain the ‘reification’ function mapping semantic values back to syntax (parameterized with the type of a given term):

↓_{b}  = λu^{Λ_{b}}.u
↓_{T_{1}→T_{2}} = λu^{Λ_{T_{1}→T_{2}}×(Λ_{T_{1}}→τ(R_{T_{1}})→τ(R_{T_{2}}))}.fst u

The complete program is the composition of the two functions and it is therefore an instance of (weak head) normalization by evaluation:

[[p_{t^{T}}]] = ↓_{T} (eval_{t,ε} εε)

In this presentation of the evaluation function there are two environments, represented by the vectors t⃗ and u⃗, whose elements can be substituted for the respective variables in the vector x⃗ (by construction, the length of all the vectors is the same). The program produces weak head normal forms, according to the call-by-name strategy given by the axioms, and it is correct in the sense that the formula Ev(t, [[p_{t^{T}}]]) is provable in M_{1}^{−}(λ) for every closed simply typed term t of type T.

3.3 Call-by-value evaluation

The process of call-by-value evaluation of closed terms is defined through the following axioms:

(A_{1}) {∀s}. V(s) → Rd(APP(LAM x_{i}. t, s), t [s/VAR x_{i}])
(A_{2}) {∀rst}. Rd(r, s) → Rd(APP(r, t), APP(s, t))
(A′_{2}) {∀rst}. V(r) → Rd(s, t) → Rd(APP(r, s), APP(r, t))
(A_{4}) V(t) for all terms t = LAM x_{i}. s

Similarly to the call-by-name case, these axioms directly encode the definition of one-step call-by-value evaluation strategy. In this case, however, the predicate Ev cannot be taken as primitive anymore, because we need to know more about the evaluation process. Informally, this is due to the fact that under call by value—in order for the proof to go through—we have to verify that whenever r reduces to s in zero or more steps, and R_{T} (r) holds, then also R_{T} (s) holds. Thus we need to proceed by induction on the length of the reduction sequence r → … → s.

To this end we define an auxiliary relation Rd_{n}^{∗}:

Rd_{0}^{∗} (t, s) := t = s
Rd_{n+1}^{∗} (t, s) := ∃r. Rd(t, r) ∧ Rd_{n}^{∗}(r, s)

A formula Rd_{n}^{∗}(t, s) is to be understood as “t reduces to s in n steps.” Just as for the simple types, we do not formalize the induction on natural numbers used in proofs of properties of Rd_{n}^{∗}—it is done at the meta level.

Then we can define the evaluation predicate as follows:

Ev_{n}(t, v) := Rd_{n}^{∗}(t, v) ∧ V(v)

This definition requires extending the logic M_{1} with the usual axioms for equality (the soundness of modified realizability is preserved with this extension [14]).

3.3.1 Computationally irrelevant existential variables

The problem with the above specification of the predicate Ev_{n} is that via modified realizability a witness to the formula ∃v. Ev_{n}(t, v) will be a sequence of terms, representing the whole reduction sequence t → … → v, while we are only interested in the final result, i.e., v. To rectify this, we introduce a further refinement of the program extraction procedure that allows to choose which of the existential quantifiers in a formula we want to realize. We use the same notation {} for “uninteresting” existential variables as that for computationally redundant universal variables. In his work on Uniform Heyting Arithmetic [3], Berger independently proposed a similar refinement.

Definition 3.9 [Computationally irrelevant existential variables] Let us define an extension of the logic M_{1} by adding formulas of the form {∃x}. ϕ, and the corresponding introduction and elimination rules:

(∃^{+}) ⟨{t}, d^{ϕ [t/x]}⟩^{{∃x}. ϕ}
(∃^{−}) [e^{{∃x}. ϕ}, u^{ϕ}.d^{ψ}]^{ψ}
(provided x ∉ FV(ψ), x ∉ FV(χ) for every v^{χ} ∈ FA(d) \ {u^{ϕ}}
and x ∉ CV(d))

Here the set of computationally relevant variables extends the previous definition in the following way:

CV([e^{{∃x}. ϕ}, u^{ϕ}.d^{ψ}]) := CV(d) ∪ CV(e)
CV(⟨{t}, d^{ϕ [t/x]}⟩) := CV(d)

The type of realizers for these new formulas is defined as τ({∃x}. ϕ) := τ(ϕ). Furthermore, r mr {∃x}. ϕ := ∃x. r mr ϕ (with x ∉ FV(r)), and

\begin{aligned}[[⟨\{t\}, d⟩]] & := & [[d]] \\ [[[e^{\{∃x\}. ϕ}, u.d]]] & := & [[d]] [[[e]]/x_{u}] \end{aligned}

Example 3.10 The formula ({∃x}. P (x)) → ∃x. P (x) is not provable: intuitively, the witness for the succedent is exactly the one provided by the proof of the antecedent of the implication, and since we do not want to know what that witness is, we also cannot produce a witness for the succedent (in other words, the witness for {∃x}. P (x) is local to the proof of this formula).

On the other hand, the formula (∃x. P (x)) → {∃x}. P (x) is provable, but it does not have any computational content if P is a Harrop formula; otherwise the extracted program is a function that only “forgets” the existential witness.

The proof of soundness for modified realizability (Theorem 2.3) can be extended to handle the additional cases.

3.3.2 Formalizing the proof

Having introduced the necessary refinement, we are now in a position to redefine the reducibility predicate in the following way (making the existential variables computationally irrelevant):

Rd_{0}^{∗} (t, s) := t = s
Rd_{n+1}^{∗} (t, s) := {∃r}. Rd(t, r) ∧ Rd_{n}^{∗}(r, s)

We can see that the type of realizers for Rd_{n}^{∗}(t, s) is now the unit type.

As remarked before, the logical relation used in the proof is defined as in the call-by-name case, except that now it can be refined—the universal variable becomes computationally redundant under call by value (we announce it in advance, but this observation can only be made after we actually write down the proof):

R_{b}(t)  := ∃v.Ev_{n}(t, v)
R_{T_{1}→T_{2}}(t) := ∃v.Ev_{n}(t, v) ∧ {∀s}. R_{T_{1}}(s) → R_{T_{2}}(APP(t, s))

For simplicity, we omit the parameterization of R_{T} by natural numbers, induced by the definition of the predicate Ev_{n}.

The call-by-value analog of Lemma 3.5 is stated and proved in the same way:

Lemma 3.11 {∀t}. R_{T} (t) → ∃v. Ev_{n}(t, v).

In order to prove the call-by-value version of Theorem 3.8 we need a few more properties of evaluation, stated in Lemmas 3.12-3.15.

Lemma 3.12 {∀st}. Rd(s, t) → R_{T} (t) → R_{T} (s).

Proof. Induction on types, using the following property: {∀stv}. Rd(s, t) → Rd_{n}^{∗}(t, v) → Rd_{n+1}^{∗} (s, v), which itself is proved by induction on n. □

Lemma 3.13 {∀st}. Rd_{n}^{∗}(s, t) → R_{T} (t) → R_{T} (s).

Proof. Induction on n, using Lemma 3.12. □

Lemma 3.14 {∀stv}. Rd_{n}^{∗}(s, v) → V(t) → Rd_{n}^{∗}(APP(t, s), APP(t, v)).

Proof. Induction on n. □

Lemma 3.15 {∀st}. Rd_{n}^{∗}(s, t) → R_{T} (s) → R_{T} (t), where m ≥ n.

Proof. Induction on n, using the following properties:

(i) {∀rst}. Rd_{n+1}^{∗} (t, s) → Rd(t, r) → Rd_{n}^{∗}(r, s)

(ii) {∀st}. Rd(t, s) → R_{T} (t) → R_{T} (s)

The proof of Property i requires an additional axiom expressing determinism of the reduction relation:

(Det) {∀rst}. Rd(t, r) → Rd(t, s) → r = s.
□

The call-by-value analog of Lemma 3.7 is stated just as before, and its proof— which we omit for lack of space—relies on Lemmas 3.12-3.15:

Lemma 3.16 For any term t of type T, with FV(t) = {x_{1}, …, x_{n}}, and for any n-tuple of closed terms r⃗ = r_{1}, …, r_{n} of types T_{i} such that R_{T_{i}}(r_{i}) holds for all 1 ≤ i ≤ n, we have

R_{T} (t [r⃗/x⃗]).

The main theorem is also stated and proved as before.

3.3.3 Extracted program

Again we see that the types τ(R_{T} (t)) are independent of t. They describe the domains of a glueing model as follows:

τ(R_{b})  := Λ_{b}
τ(R_{T_{1}→T_{2}}) := Λ_{T_{1}→T_{2}} × (τ(R_{T_{1}}) → τ(R_{T_{2}}))

Similarly to the previous case, the program we obtain for call by value is the composition of the term extracted from Lemma 3.11 (the same as for call by name), and the one extracted from Lemma 3.16, which looks as follows:

eval_{VAR x_{i},x⃗}  = λt⃗u⃗.u_{i}
eval_{APP(r,s),x⃗}  = λt⃗u⃗.snd(eval_{r,x⃗} t⃗u⃗) (eval_{s,x⃗} t⃗u⃗)
eval_{LAM x_{n+1}^{T_{1}}. t^{T_{2}},x⃗} = λt⃗u⃗.((LAM x_{n+1}. t) [t⃗/x⃗], λv.eval_{t,x⃗x_{n+1}} (t⃗(↓_{T_{1}} v))(u⃗v))

This program also threads two environments, but the first of them (represented by the vector t⃗) contains already evaluated terms. As before, for every closed term t^{Λ_{T}}, eval_{t,ε} denotes the glueing model interpretation of the object-level term denoted by t^{Λ_{T}}.

Remark 3.17 In the original formulation of Lemma 3.16 in Pierce’s book [12, p. 151], the terms to be substituted for free variables in a given term were required to be values. This restriction, however, is not necessary for the proof to go through, and the resulting program is exactly the same as the one obtained here.

3.4 Weak head normalization for closed terms of base type

We now show a variant of the proof of weak head normalization where we are only interested in evaluating terms of base type. In order to be able to observe the behavior of programs, we extend the object language with integers, formed with the zero constant 0 and the successor constant S in the usual way. The set of base types now includes the type ι for integers. As mentioned before, for call-by-name evaluation we can simplify the definition of the relation R_{T}, which consequently leads to a simpler extracted program that we will show next.

We add the following two axioms specifying the evaluation strategy for the new terms:

(A_{5}) Ev(0, 0)
(A_{6}) ∀tv. Ev(t, v) → Ev(S t, S v)

The definition of the logical relation is now less restrictive for higher types:

R_{b}(t)  := ∃v.Ev(t, v)
R_{T_{1}→T_{2}}(t) := {∀s}. R_{T_{1}}(s) → R_{T_{2}}(APP(t, s))

Theorem 3.18 For any closed term t of type ι, ∃v.Ev(t, v) holds.

The proof is carried out almost as before, and it relies on the base-type version of Lemma 3.5, on Lemma 3.6 as before, and on the base-type counterpart of Lemma 3.7 which now reads as follows (note that the vector of terms r⃗ is now computationally redundant):

Lemma 3.19 For any term t of type T, with FV(t) = {x_{1}, …, x_{n}},

{∀r⃗}. (R_{T_{1}}(r_{1}) ∧ … ∧ R_{T_{n}}(r_{n})) → R_{T} (t [r⃗/x⃗]).

For the proof of Lemma 3.19 we need to show that R_{ι}(0) holds, and that for any term t of type ι, R_{ι}(t) → R_{ι}(S t) holds.

Remark 3.20 The proof does not go through if we use the call-by-value axiomatization instead of call by name; this is due to the fact that in the proof of the main lemma, in the case for abstraction, we must know that an arbitrary term of an arbitrary type evaluates to a value. However, with the weakened definition of the relation R_{T} we cannot prove this fact any more.

The program extracted from the proof looks as follows:

eval_{0,x⃗}  = λu⃗.0
eval_{S t,x⃗}  = λu⃗.S (eval_{t,x⃗} u⃗)
eval_{VAR x_{i},x⃗}  = λu⃗.u_{i}
eval_{APP(r,s),x⃗} = λu⃗.(eval_{r,x⃗} u⃗) (eval_{s,x⃗} u⃗)
eval_{LAM x_{n+1}. t,x⃗} = λu⃗.λv.eval_{t,x⃗x_{n+1}} u⃗v

Acknowledgments:

We are grateful to Dariusz Biernacki, Philipp Gerhardy, and the MFPS reviewers for their comprehensive feedback. Special thanks to Andrzej Filinski for two rounds of insightful comments.

This work is partially supported by the ESPRIT Working Group APPSEM II (http://www.appsem.org) and by the Danish Natural Science Research Council, Grant no. 21-03-0545.

A Implementation

This appendix contains an ML implementation of the normalization programs from Sections 3.2.2 and 3.3.3. The implementation ignores the dependencies in the definition of the object-level terms and the semantic domains:

   type ide = string
   datatype term = VAR of ide
                 | APP of term * term
                 | LAM of ide * term

The ML programs work by optimistically trying to interpret an untyped object-level term (defined in the data type term just above) into a semantic domain defined by a reflexive type (see the data type R below for call by name and call by value). However, as stressed by Filinski [9,10], it is a non-trivial task to prove that such implementations are correct.

We use the following auxiliary functions, whose definitions are omitted:

   subst_all : term * (ide * term) list -> term
   lookup : ''a * (''a * 'b) list -> 'b

The function subst all implements simultaneous substitution of terms for variables. The function lookup implements a standard association-list lookup.

A.1 Call by name

datatype R = BASE of term
       | ARROW of term * (term -> R -> R)
fun reify (BASE t)
= t
| reify (ARROW (t, f))
= t
fun eval (VAR x, ts, us)
= lookup (x, us)
| eval (APP (t1, t2), ts, us)
= let val ARROW (_, f) = eval (t1, ts, us)
  in f (subst_all (t2, ts)) (eval (t2, ts, us))
  end
| eval (LAM (y, t1), ts, us)
= let val t = subst_all (LAM (y, t1), ts)
      val f = fn s => fn u => eval (t1, (y, s) :: ts, (y, u) :: us)
  in ARROW (t, f)
  end
fun normalize t
= reify (eval (t, [], []))

A.2 Call by value

datatype R = BASE of term
       | ARROW of term * (R -> R)
fun reify (BASE t)
= t
| reify (ARROW (t, f))
= t
fun eval (VAR x, ts, us)
= lookup (x, us)
| eval (APP (t1, t2), ts, us)
= let val ARROW (_, f) = eval (t1, ts, us)
  in f (eval (t2, ts, us))
  end
| eval (LAM (y, t1), ts, us)
= let val t = subst_all (LAM (y, t1), ts)
      val f = fn u => eval (t1, (y, reify u) :: ts, (y, u) :: us)
  in ARROW (t, f)
  end
fun normalize t
= reify (eval (t, [], []))

References

[1] Barendregt, H., “The Lambda Calculus: Its Syntax and Semantics,” Studies in Logic and the Foundation of Mathematics 103, North-Holland, 1984, revised edition.

[2] Berger, U., 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 (1993), pp. 91–106.

[3] Berger, U., Uniform Heyting arithmetic, Annals of Pure and Applied Logic 133 (2005), pp. 125–148.

[4] Berger, U., W. Buchholz and H. Schwichtenberg, Refined program extraction from classical proofs, Annals of Pure and Applied Logic 114 (2002), pp. 3–25.

[5] Berger, U. and H. Schwichtenberg, An inverse of the evaluation functional for typed λ-calculus, in: G. Kahn, editor, Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science (1991), pp. 203–211.

[6] Biernacka, M., O. Danvy and K. Støvring, Extracting evaluators from proofs of weak head normalization, Research Report BRICS RS-05-12, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark (2005), extended version of an article to appear in the preliminary proceedings of MFPS XXI, Birmingham, UK, May 2005.

[7] Coquand, T. and P. Dybjer, Intuitionistic model constructions and normalization proofs, in: International Workshop TYPES’93, Nijmegen, The Netherlands, 1993,

available at http://www.cs.chalmers.se/~peterd/papers/nbe.html.

[8] Coquand, T. and P. Dybjer, Intuitionistic model constructions and normalization proofs, Mathematical Structures in Computer Science 7 (1997), pp. 75–94.

[9] Dybjer, P. and A. Filinski, Normalization and partial evaluation, in: G. Barthe, P. Dybjer, L. Pinto and J. Saraiva, editors, Applied Semantics – Advanced Lectures, number 2395 in Lecture Notes in Computer Science (2000), pp. 137– 192.

[10] Filinski, A. and H. K. Rohde, A denotational account of untyped normalization by evaluation, in: I. Walukiewicz, editor, Foundations of Software Science and Computation Structures, 7th International Conference, FOSSACS 2004, number 2987 in Lecture Notes in Computer Science (2002), pp. 167–181.

[11] Kreisel, G., Interpretation of analysis by means of functionals of finite type, in: Constructivity in Mathematics, Proc. Colloq. Amsterdam (1957), Studies in Logic and the Foundation of Mathematics (1959), pp. 101–128.

[12] Pierce, B. C., “Types and Programming Languages,” The MIT Press, 2002.

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

[14] Troelstra, A. S., editor, “Metamathematical Investigation of Intuitionistic Arithmetic and Analysis,” Lecture Notes in Mathematics 344, Springer-Verlag, 1973.

Recent BRICS Report Series Publications

RS-05-12 Ma�gorzata Biernacka, Olivier Danvy, and Kristian Støvring. Program Extraction from Proofs of Weak Head Normalization. April 2005. 19 pp. Extended version of an article to appear in the preliminary proceedings of MFPS XXI, Birmingham, UK, May 2005.

RS-05-11 Ma�gorzata Biernacka, Dariusz Biernacki, and Olivier Danvy. An Operational Foundation for Delimited Continuations in the CPS Hierarchy. March 2005. iii+42 pp. A preliminary version appeared in Thielecke, editor, 4th ACM SIGPLAN Workshop on Continuations, CW ’04 Proceedings, Association for Computing Machinery (ACM) SIGPLAN Technical Reports CSR-04-1, 2004, pages 25–33. This version supersedes BRICS RS-04-29.

RS-05-10 Dariusz Biernacki and Olivier Danvy. A Simple Proof of a Folklore Theorem about Delimited Control. March 2005. ii+11 pp.

RS-05-9 Gudmund Skovbjerg Frandsen and Peter Bro Miltersen. Reviewing Bounds on the Circuit Size of the Hardest Functions. March 2005. 6 pp. To appear in Information Processing Letters.

RS-05-8 Peter D. Mosses. Exploiting Labels in Structural Operational Semantics. February 2005. 15 pp. Appears in Fundamenta Informaticae, 60:17–31, 2004.

RS-05-7 Peter D. Mosses. Modular Structural Operational Semantics. February 2005. 46 pp. Appears in Journal of Logic and Algebraic Programming, 60–61:195–228, 2004.

RS-05-6 Karl Krukow and Andrew Twigg. Distributed Approximation of Fixed-Points in Trust Structures. February 2005. 41 pp.

RS-05-5 A Dynamic Continuation-Passing Style for Dynamic Delimited Continuations. Dariusz Biernacki and Olivier Danvy and Kevin Millikin. February 2005.

RS-05-4 Andrzej Filinski and Henning Korsholm Rohde. Denotational Aspects of Untyped Normalization by Evaluation. February 2005. 51 pp. Extended version of an article to appear in the FOSSACS 2004 special issue of RAIRO, Theoretical Informatics and Applications.