BRICS

Basic Research in Computer Science

A Syntactic Correspondence between Context-Sensitive Calculi and Abstract Machines

Ma�gorzata Biernacka Olivier Danvy

BRICS Report Series RS-05-38 ISSN 0909-0878 December 2005 BRICS RS-05-38 Biernacka & Danvy: A Syntactic Correspondence between Context-Sensitive Calculi and Abstract Machines Copyright \begin{matrix}c \\ ◯ \end{matrix} 2005, Ma�gorzata Biernacka & 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/05/38/

A Syntactic Correspondence between Context-Sensitive Calculi and Abstract Machines

Małgorzata Biernacka and Olivier Danvy BRICS^{∗} Department of Computer Science University of Aarhus^{†}

December 27, 2005

Abstract

We present a systematic construction of environment-based abstract machines from context-sensitive calculi of explicit substitutions, and we illustrate it with ten calculi and machines for applicative order with an abort operation, normal order with generalized reduction and call/cc, the lambda-mu-calculus, delimited continuations, stack inspection, proper tail-recursion, and lazy evaluation. Most of the machines already exist but have been obtained independently and are only indirectly related to the corresponding calculi. All of the calculi are new and they make it possible to directly reason about the execution of the corresponding machines.

In connection with the functional correspondence between evaluation functions and abstract machines initiated by Reynolds, the present syntactic correspondence makes it possible to construct reduction-free normalization functions out of reductionbased ones, which was an open problem in the area of normalization by evaluation.

Revised version of BRICS RS-05-22.

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

† IT-parken, Aabogade 34, DK-8200 Aarhus N, Denmark.

Email: {mbiernac,danvy}@brics.dk

Contents

1 Introduction 1 1.1 Calculi and machines . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 Calculi of explicit substitutions and environment-based machines . . . . . . 2 1.3 Calculi of explicit substitutions for computational effects and environment-

based machines . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.4 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2

2 Preliminaries 3 2.1 Reduction semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 2.2 Context-sensitive reduction . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 2.3 Our base calculus of closures: λρ̂ . . . . . . . . . . . . . . . . . . . . . . . . 4

3 The λρ̂A-calculus 5

3.1 A reduction semantics for applicative order and abort . . . . . . . . . . . . 6 3.1.1 Decomposition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 3.1.2 Context-sensitive contraction . . . . . . . . . . . . . . . . . . . . . . 7 3.1.3 Plugging . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 3.1.4 One-step reduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 3.1.5 Reduction-based evaluation . . . . . . . . . . . . . . . . . . . . . . . 8

3.2 A pre-abstract machine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 3.3 A staged abstract machine . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 3.4 An eval/apply abstract machine . . . . . . . . . . . . . . . . . . . . . . . . . 11 3.5 Transition compression . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 3.6 An environment machine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 3.7 Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 3.8 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12

4 The λρ̂K-calculus 13 4.1 The language of λρ̂K . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 4.2 Notion of context-sensitive reduction . . . . . . . . . . . . . . . . . . . . . . 13 4.3 Krivine’s machine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 4.4 Formal correspondence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14

5 The λρ̂μ-calculus 14 5.1 The language of λρ̂μ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 5.2 Notion of context-sensitive reduction . . . . . . . . . . . . . . . . . . . . . . 15 5.3 An eval/apply abstract machine . . . . . . . . . . . . . . . . . . . . . . . . . 15 5.4 Formal correspondence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16

6 Delimited continuations 16

6.1 The λρ̂S-calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 6.1.1 The language of λρ̂S . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 6.1.2 The eval/apply/meta-apply abstract machine . . . . . . . . . . . . . 17 6.1.3 Notion of context-sensitive reduction . . . . . . . . . . . . . . . . . . 18 6.1.4 Formal correspondence . . . . . . . . . . . . . . . . . . . . . . . . . . 18 6.1.5 The CPS hierarchy . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18

6.2 The λρ̂F-calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 6.2.1 The language of λρ̂F . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 6.2.2 Notion of context-sensitive reduction . . . . . . . . . . . . . . . . . . 19 6.2.3 The eval/apply abstract machine . . . . . . . . . . . . . . . . . . . . 20 6.2.4 Formal correspondence . . . . . . . . . . . . . . . . . . . . . . . . . . 20 6.2.5 A hierarchy of control delimiters . . . . . . . . . . . . . . . . . . . . 20

6.3 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20

7 Stack inspection 22

7.1 The λρ̂_{sec}-calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 7.1.1 The language of λρ̂_{sec} . . . . . . . . . . . . . . . . . . . . . . . . . . 22 7.1.2 Notion of context-sensitive reduction . . . . . . . . . . . . . . . . . . 22 7.1.3 An eval/apply abstract machine . . . . . . . . . . . . . . . . . . . . 23 7.1.4 Formal correspondence . . . . . . . . . . . . . . . . . . . . . . . . . . 23

7.2 Properly tail-recursive stack inspection . . . . . . . . . . . . . . . . . . . . . 23 7.2.1 The storeless cm machine . . . . . . . . . . . . . . . . . . . . . . . . 24 7.2.2 The underlying calculus λρ_{sec}^{cm} . . . . . . . . . . . . . . . . . . . . . . 24

7.3 State-based properly tail-recursive stack inspection . . . . . . . . . . . . . . 25 7.3.1 The unzipped storeless cm machine . . . . . . . . . . . . . . . . . . . 25 7.3.2 The language of λρ_{sec}^{ucm} . . . . . . . . . . . . . . . . . . . . . . . . . . 26 7.3.3 Notion of context-sensitive reduction . . . . . . . . . . . . . . . . . . 26 7.3.4 Formal correspondence . . . . . . . . . . . . . . . . . . . . . . . . . . 27

7.4 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27

8 A calculus for proper tail-recursion 27 8.1 A simplified version of Clinger’s abstract machine . . . . . . . . . . . . . . . 27 8.2 The language of λρ̂_{ptr} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 8.3 Notion of context-sensitive reduction . . . . . . . . . . . . . . . . . . . . . . 28 8.4 Formal correspondence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28

9 A lazy calculus of closures 29 9.1 The language of λρ̂_{l} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 9.2 Notion of context-sensitive reduction . . . . . . . . . . . . . . . . . . . . . . 29 9.3 An eval/apply abstract machine . . . . . . . . . . . . . . . . . . . . . . . . . 29 9.4 Formal correspondence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30

10 Conclusion 30

1 Introduction

How does one construct a new semantic artifact?

1.1 Calculi and machines

Sixty-five years ago, the λ-calculus was introduced [15]. Forty-five years ago, its expressive power was observed to be relevant for computing [67,81]. Forty years ago, a first abstract machine for the λ-calculus was introduced [61]. Thirty years ago, calculi and abstract machines were formally connected [70]. Twenty years ago, a calculus format—reduction semantics—with an explicit representation of reduction contexts was introduced [40]. Today calculi and abstract machines are standard tools to study programming languages. Given a calculus, it is by now a standard activity to design a corresponding abstract machine and to prove its correctness [42].

From calculus to machine by refocusing and transition compression: Recently, Danvy and Nielsen have pointed out that the reduction strategy for a calculus actually determines the structure of the corresponding machine [36]. They present a method for constructing an abstract machine out of a reduction semantics satisfying the uniquedecomposition property. In such a reduction semantics, a non-value term is reduced by

1. decomposing it (uniquely) into a redex and its context,

2. contracting the redex, and

3. plugging the contractum into the reduction context,

yielding a new term. A reduction-based evaluation function is defined using the reflexive and transitive closure of the one-step reduction function:

[figure: ∘; decompose; ∘; decompose; ∘; decompose; ∘; contract; ∘; plug; ∘; contract; ∘; plug; ∘; contract]

Danvy and Nielsen have observed that the intermediate terms, in the composition of plug and decompose, could be avoided by fusing the composition into a ‘refocus’ function:

[figure: ∘; decompose; ∘; decompose; ∘; decompose; ∘; contract; ∘; plug; refocus; ∘; contract; ∘; plug; refocus; ∘; contract]

The resulting ‘refocused’ evaluation function is defined as the reflexive and transitive closure of refocusing and contraction.

The refocus function takes the form of a state-transition function, i.e., an abstract machine. The refocused evaluation function therefore also takes the form of an abstract machine. Compressing its intermediate transitions (i.e., short-circuiting them) yields abstract machines that are often independently known: for example, for the pure λ-calculus with normal order, the resulting abstract machine is a substitution-based version of the Krivine machine (i.e., a push/enter machine); for the pure λ-calculus with applicative order, the resulting abstract machine is Felleisen et al.’s CK machine (i.e., an eval/apply machine). Refocusing has also been applied to the term language of the free monoid, yielding a reduction-free normalization function [26], and to context-based CPS transformations, improving them from quadratic time to operating in one pass [36].

1.2 Calculi of explicit substitutions and environment-based machines

Twenty years ago, Curien observed that while most calculi use actual substitutions, most implementations use closures and environments [22]. He then developed a calculus of closures, λρ [23], thereby launching the study of explicit substitutions [1, 24, 51, 65, 75].

From calculus to machine by refocusing, transition compression, and closure unfolding: Recently, we have applied the refocusing method to λρ̂, a minimal extension of λρ where one can express single-step computations; we added an unfolding step to make the machine operate not on a closure, but on a term and its environment [8]. We have shown how λρ̂ with left-to-right applicative order directly corresponds to the CEK machine [43], how λρ̂ with normal order directly corresponds to the Krivine machine [20, 23], how λρ̂ with generalized reduction directly corresponds to the original version of Krivine’s machine [59], and how λρ̂ with right-to-left applicative order directly corresponds to the ZINC abstract machine [64]. All of these machines are environment-based and use closures.

1.3 Calculi of explicit substitutions for computational effects and environment-based machines

Twenty years ago, Felleisen introduced reduction semantics—a version of small-step operational semantics with an explicit representation of reduction contexts—in order to provide calculi for control and state [40, 43]. In these calculi, reduction rules are not oblivious to their reduction context; on the contrary, they are \underline{context} \underline{sensitive} in that the context takes part in some reduction steps, e.g., for call/cc. Reduction semantics are in wide use today, e.g., to study the security technique of stack inspection [16, 47, 71].

From calculus to machine by refocusing, transition compression, and closure unfolding: In this article, we apply the refocusing method to context-sensitive extensions of λρ̂ accounting for a variety of computational effects. We present ten calculi of closures and the corresponding environment-based machines. What is significant here is that each machine is mechanically derived from the corresponding calculus (instead of designed and then proved correct) and also that each machine directly corresponds to this calculus (instead of indirectly via an ‘unload’ function at the end of each run [70] or via a compilation / decompilation scheme in the course of execution [51]).

1.4 Overview

We successively consider call by name: Krivine’s machine with call/cc (Section 4) and the λμ-calculus (Section 5); call by value: static and dynamic delimited continuations (Section 6), stack inspection (Section 7), and proper tail-recursion (Section 8); and call by need (Section 9). Towards this end, we first present the λρ̂-calculus and the notion of context-sensitive reduction (Section 2) and then a detailed walkthrough for the λρ̂- calculus with an abort operation (Section 3). The subsequent repetitiveness of Sections 4 to 9 (language, notion of context-sensitive reduction, abstract machine, and formal correspondence) is a deliberate feature, not an inadvertent presentational bug: we apply the same simple method to many situations that have been separately studied so far. Each of these sections can therefore be read independently of the others.

2 Preliminaries

2.1 Reduction semantics

A reduction semantics [40, 42] consists of a grammar of terms from a source language, syntactic notions of value and redex, a collection of contraction rules, and a reduction strategy. This reduction strategy is embodied in a grammar of reduction contexts (terms with a hole as induced by the compatibility rules) and a plug function mapping a term and a context into a new term. One-step reduction of a non-value term consists in

1. decomposing the term into a redex and a reduction context,

2. contracting the redex, and

3. plugging the contractum in the reduction context.

In some reduction semantics, non-value terms are uniquely decomposed into a redex and a context. Decomposition can then be implemented as a function mapping a non-value term to a redex and a reduction context. Danvy and Nielsen have shown that together with the unique decomposition property, the following property of a reduction semantics is sufficient to define a decomposition function by induction on terms and reduction contexts [36, Figure 2, page 8]:

Property 1. For each syntactic construct building a term out of n subterms, there is a number 0 ≤ i ≤ n and a fixed traversal order of subterms encoded in the grammar of the reduction contexts for this construct such that the holes of these contexts are precisely the positions of the i subterms. Furthermore, a term with all the chosen i subterms reduced to values is either a value or a potential redex (i.e., an actual redex or a “stuck term”) but not both.

If the redexes do not overlap, the contraction rules can be implemented as a function.

2.2 Context-sensitive reduction

Traditional specifications of one-step reduction as the compatible closure of a notion of reduction provide a local characterization of a computation step in the form of a redex.^{1} This local characterization is not fit for non-local reductions such as one involving a control operator capturing all its surrounding context in one step, or a global state. For these, one needs a notion of context-sensitive reduction, i.e., a binary relation defined both on redexes and on their reduction context instead of only on redexes [40].

This relation is given by context-sensitive contraction rules of the form ⟨r, C ⟩ → ⟨c′, C′⟩, where ⟨r, C ⟩ denotes the decomposition of a program into a potential redex r and its context C .

A one-step reduction relation for a given notion of context-sensitive reduction is defined as follows: A program p reduces in one step to p′ if decomposing p yields ⟨r, C ⟩, reducing ⟨r, C ⟩ yields ⟨c′, C′⟩, and plugging c′ into C′ yields p′.

A context-sensitive reduction implicitly assumes a decomposition of the entire program, and therefore it cannot be used locally. One way to recover compatibility in the contextsensitive setting is to add explicit local control delimiters to the language (see Section 6 for an illustration). For a language without explicit control delimiters (as the λρ̂-calculus with call/cc), there is an implicit global control delimiter around the program [41].

1For example, a potential redex in the λ-calculus is the application of a value to a term. If the value is a λ-abstraction, the potential redex is an actual one and it can be β-reduced. If no reduction rule applies, the potential redex is not an actual one and the program is stuck [70].

2.3 Our base calculus of closures: λρ̂

Since Landin [61], most abstract machines implementing variants and extensions of the λ-calculus use closures and environments, and the substitution of terms for free variables is thus delayed until a variable is reached in the evaluation process. This implementation technique has motivated the study of calculi of explicit substitutions [1,23,75] to mediate between the traditional abstract specifications of the λ-calculus and its traditional concrete implementations [51].

To derive an abstract machine for evaluating λ-terms, a weak calculus of explicit substitutions suffices. The first (and simplest) of such calculi was Curien’s calculus of closures λρ [23]. Although this calculus is not expressive enough to model full normalization, it is suitable for evaluating a λ-term, i.e., to produce the corresponding weak head normal form. Its operational semantics is specified using multi-step reductions, but its syntax is too restrictive to allow single-step computations, which is what we need to apply the refocusing method. For this reason, in our earlier work [8], we have proposed a minimal extension of λρ with one-step reduction rules, the λρ̂-calculus.

The language of λρ̂ is as follows:

(terms)  t ::= i | λt | t t
(closures)  c ::= t[s] | c c
(substitutions) s ::= • | c · s

(For comparison, λρ does not have the c c production.)

We use de Bruijn indices for variables in a term (i ≥ 1). A closure is a term equipped with a substitution, i.e., a list of closures to be substituted for free variables in the term. Programs are closures of the form t[•] where t does not contain free variables.

The notion of reduction in the λρ̂-calculus is given by the following rules:

(Var) i[c_{1} ⋯ c_{j}] \underrightarrow{ρ̂} c_{i} if i ≤ j
(Beta) ((λt)[s]) c \underrightarrow{ρ̂} t[c · s]
(Prop) (t_{0} t_{1})[s] \underrightarrow{ρ̂} (t_{0}[s]) (t_{1}[s])

We write s(i) for the ith element of the substitution s considered as a list. (So [c_{1} ⋯ c_{j}](i) = c_{i} if 1 ≤ i ≤ j.)

Finally, the one-step reduction relation (i.e., the compatible closure of the notion of reduction) extends the notion of reduction with the following rules:

(L-Comp)  \frac{c_{0} \underrightarrow{ρ̂} c′_{0}}{c_{0} c_{1} \underrightarrow{ρ̂} c′_{0} c_{1}}

(R-Comp)  \frac{c_{1} \underrightarrow{ρ̂} c′_{1}}{c_{0} c_{1} \underrightarrow{ρ̂} c_{0} c′_{1}}

(Sub)  \frac{c_{i} \underrightarrow{ρ̂} c′_{i}}{t[c_{1} ⋯ c_{i} ⋯ c_{j}] \underrightarrow{ρ̂} t[c_{1} ⋯ c′_{i} ⋯ c_{j}]} for i ≤ j

Specific, deterministic reduction strategies can be obtained by restricting the compatibility rules. In the following sections, we consider two such strategies:

1. the normal-order strategy obtained by discarding the (Sub) and (R-Comp) rules, where the grammars of values, redexes and reduction contexts are specified as follows:

(values)  v ::= (λt)[s]
(redexes)  r ::= v c | i[s] | (t_{0} t_{1})[s]
(reduction contexts) C ::= [ ] | C [[ ] c],

and

2. the left-to-right applicative-order strategy obtained in the usual way by discarding the (Sub) rule and restricting the (Beta) and (R-Comp) rules, where the grammars of values, redexes and reduction contexts are specified as follows:

(values)  v ::= (λt)[s]
(redexes)  r ::= v v | i[s] | (t_{0} t_{1})[s]
(reduction contexts) C ::= [ ] | C [[ ] c] | C [v [ ]]

All of the calculi presented in this article extend the λρ̂-calculus. For each of them, we define a suitable notion of reduction, denoted →_{X}, where X is a subscript identifying a particular calculus. For each of them, we then define a one-step reduction relation as the composition of: decomposing a non-value closure into a redex and a reduction context, contracting a (context-sensitive) redex, and then plugging the resulting closure into the resulting context. Finally, we define the evaluation relation (denoted →_{X}^{∗}) using the reflexive, transitive closure of one-step reduction, i.e., we say that c evaluates to c′ if c →_{X}^{∗} c′ and c′ is a value closure. We define the convertibility relation between closures as the smallest equivalence relation containing →_{X}^{∗}. If two closures c and c′ are convertible, they behave similarly under evaluation (i.e., either they both evaluate to the same value, or they both diverge).

3 The λρ̂A-calculus

As an illustration, we present a detailed and systematic derivation of an abstract machine for call-by-value evaluation in the λ-calculus with an abort operation, starting from the specification of the applicative-order reduction strategy in the λρ̂-calculus with an abort operation. We follow the steps outlined by Biernacka, Danvy, and Nielsen [8, 36]:

Section 3.1: We specify the applicative-order reduction strategy in the form of a reduction semantics, i.e., with a one-step reduction function specified as decomposing a nonvalue term into a reduction context and a redex, contracting this redex, and plugging the contractum into the context. As is traditional, we also specify evaluation as the transitive closure of one-step reduction.

Section 3.2: We replace the combination of plugging and decomposition by a refocus function that iteratively goes from redex site to redex site in the reduction sequence. The resulting ‘refocused’ evaluation function is the transitive closure of the refocus function and takes the form of a ‘pre-abstract machine.’

Section 3.3: We merge the definitions of the transitive closure and the refocus function into a ‘staged abstract machine’ that implements the reduction rules and the compatibility rules of the λρ̂-calculus with two separate transition functions.

Section 3.4: We inline the transition function implementing the reduction rules. The result is an eval/apply abstract machine consisting of an ‘eval’ transition function dispatching on closures and an ‘apply’ transition function dispatching on contexts.

Section 3.5: Observing that in a reduction sequence, an (App) reduction step is always followed by a decomposition step, we coalesce these two steps into one. Observing that in a reduction sequence, an (Abort) reduction step is always followed by a decomposition step, we coalesce these two steps into one. This shortcut makes the resulting abstract machine dispatch on terms rather than on closures, and enables the following step.

Section 3.6: We unfold the data type of closures, making the abstract machine operate over two components—a term and a substitution—instead of over one—a closure. The substitution component is the traditional environment of environment machines, and the resulting machine is an environment machine. This machine coincides with the CEK machine with an abort operator [42].

In Section 3.7, we state the correctness of the resulting CEK machine with respect to evaluation in the λρ̂-calculus with an abort operation.

3.1 A reduction semantics for applicative order and abort

A reduction semantics for applicative-order reduction in the λρ̂A-calculus builds on the applicative-order strategy presented in Section 2.3. The grammar of terms and closures contains additional productions for the abort operation:

(Term)  t ::= … | A t
(Closure)  c ::= … | A c

The reduction semantics is context-sensitive and its contraction rules contain the contractions of the λρ̂-calculus (here stated in the context-sensitive form):

(Var) ⟨i[c_{1} ⋯ c_{j}], C ⟩ →_{A} ⟨c_{i}, C ⟩ if i ≤ j
(Beta) ⟨((λt)[s]) c, C ⟩ →_{A} ⟨t[c · s], C ⟩
(Prop) ⟨(t_{0} t_{1})[s], C ⟩ →_{A} ⟨(t_{0}[s]) (t_{1}[s]), C ⟩

as well as two new contractions for the abort operation:

(Prop_{A}) ⟨(A t)[s], C ⟩ →_{A} ⟨A (t[s]), C ⟩
(Abort)  ⟨A v, C ⟩ →_{A} ⟨v, [ ]⟩

Finally, the grammar of reduction contexts reads as follows:

(Context)  C ::= [ ] | C [[ ] c] | C [v [ ]] | C [A [ ]]

This reduction semantics satisfies the conditions stated in Section 2.1. We can therefore define the following three functions:

decompose : Closure → Value + (Redex × Context)
contract : Redex × Context → Closure × Context
plug : Closure × Context → Closure

3.1.1 Decomposition We define decompose as a transition function over closures and reduction contexts:

decompose : Closure → Value + (Redex × Context)
decompose c = decompose′ (c, [ ])
decompose′ : Closure × Context → Value + (Redex × Context)
decompose′ (i[s], C ) = (i[s], C )
decompose′ ((λt)[s], C ) = decompose′_{aux} (C , (λt)[s])
decompose′ ((t_{0} t_{1})[s], C ) = ((t_{0} t_{1})[s], C )
decompose′ (c_{0} c_{1}, C ) = decompose′ (c_{0}, C [[ ] c_{1}])
decompose′ ((A t)[s], C ) = ((A t)[s], C )
decompose′ (A c, C ) = decompose′ (c, C [A [ ]])
decompose′_{aux} : Context × Value → Value + (Redex × Context)
decompose′_{aux} ([ ], v) = v
decompose′_{aux} (C [[ ] c], v) = decompose′ (c, C [v [ ]])
decompose′_{aux} (C [v′ [ ]], v) = (v′ v, C )
decompose′_{aux} (C [A [ ]], v) = (A v, C )

The main decomposition function, decompose, uses two auxiliary transition functions that work according to Property 1:

• decompose′ is passed a closure and a reduction context. It dispatches on the closure

and iteratively builds the reduction context:

– if the current closure is a value, then decompose′_{aux} is called to inspect the context;

– if the current closure is a redex, then a decomposition is found; and

– otherwise, a subclosure of the current closure is chosen to be visited in a new

context.

• decompose′_{aux} is passed a reduction context and a value. It dispatches on the reduc-

tion context:

– if the current context is empty, then the value is the result of the function;

– if the top constructor of the context is that of a function application, the actual parameter is decomposed in a new context; and

– otherwise, a redex has been found. The decomposition function is total.

3.1.2 Context-sensitive contraction We define contract by cases, as a straightforward implementation of the contraction rules:

contract : Redex × Context → Closure × Context
contract (i[v_{1} ⋯ v_{m}], C ) = (v_{i}, C )
contract ((t_{0} t_{1})[s], C ) = ((t_{0}[s]) (t_{1}[s]), C )
contract (((λt)[s]) v, C ) = (t[v · s], C )
contract ((A t)[s], C ) = (A (t[s]), C )
contract (A v, C ) = (v, [ ])

In general, the contraction function is partial because of stuck terms.

3.1.3 Plugging

We define plug by structural induction over the reduction context. It iteratively peels off the context and thus also takes the form of a transition function:

plug : Closure × Context → Closure
plug (c, [ ]) = c
plug (c_{0}, C [[ ] c_{1}]) = plug (c_{0} c_{1}, C )
plug (c_{1}, C [c_{0} [ ]]) = plug (c_{0} c_{1}, C )
plug (c, C [A [ ]]) = plug (A c, C )

The plugging function is total.

3.1.4 One-step reduction

Given these three functions, we can define the following one-step reduction function that tests whether a closure is a value or can be decomposed into a redex and a context, that contracts this redex together with its context, and that plugs the contractum in the resulting context:

reduce : Closure → Closure
reduce c =

case decompose c
of  v ⇒ v
| (r, C ) ⇒ plug (c′, C′) where (c′, C′) = contract (r, C )

In general, the one-step reduction function is partial because of the contraction function. The following proposition is a consequence of the unique-decomposition property.

Proposition 1. For any non-value closure c and for any closure c′, c →_{A} c′ ⇔ reduce c = c′.

3.1.5 Reduction-based evaluation

Finally, we can define evaluation as the reflexive, transitive closure of one-step reduction. For simplicity, we use decompose to test whether a value has been reached:

iterate : Value + (Redex × Context) → Value
iterate v = v
iterate (r, C ) = iterate (decompose (plug (c′, C′)))

where (c′, C′) = contract (r, C )

evaluate : Term → Value
evaluate t = iterate (decompose (t[•]))

This evaluation function is partial because of the one-step reduction function and also because a reduction sequence might not terminate.

Proposition 2. For any closed term t and any value v, t[•] →_{A}^{∗} v ⇔ evaluate t = v.

3.2 A pre-abstract machine

The reduction sequence implemented by evaluation can be depicted as follows:

[figure: ∘; decompose; ∘; decompose; ∘; decompose; ∘; contract; ∘; plug; ∘; contract; ∘; plug; ∘; contract; ∘]

At each step, an intermediate term is constructed by the function plug; it is then immediately decomposed by the subsequent call to decompose. In earlier work [36], Danvy and Nielsen pointed out that the composition of plug and decompose (which are total) could be replaced by a more efficient function, refocus (which is also total), that would directly go from redex site to redex site in the reduction sequence:

[figure: ∘; decompose; ∘; decompose; ∘; decompose; ∘; contract; ∘; plug; refocus; ∘; contract; ∘; plug; refocus; ∘; contract; ∘]

The essence of refocusing for a reduction semantics satisfying the unique decomposition property is captured in the following proposition:

Proposition 3 (Danvy and Nielsen [26,36]). For any closure c and reduction context C ,

decompose (plug (c, C )) = decompose′ (c, C )

In words: refocusing amounts to continuing the decomposition of the given contractum in the given context.

The definition of the refocus function is therefore a clone of that of decompose′. In particular, it involves an auxiliary function refocus_{aux} and takes the form of two statetransition functions, i.e., of an abstract machine:

refocus : Closure × Context → Value + (Redex × Context)
refocus (i[s], C ) = (i[s], C )
refocus ((λt)[s], C ) = refocus_{aux} (C , (λt)[s])
refocus ((t_{0} t_{1})[s], C ) = ((t_{0} t_{1})[s], C )
refocus (c_{0} c_{1}, C ) = refocus (c_{0}, C [[ ] c_{1}])
refocus ((A t)[s], C ) = ((A t)[s], C )
refocus (A c, C ) = refocus (c, C [A [ ]])
refocus_{aux} : Context × Value → Value + (Redex × Context)
refocus_{aux} ([ ], v) = v
refocus_{aux} (C [[ ] c], v) = refocus (c, C [v [ ]])
refocus_{aux} (C [v′ [ ]], v) = (v′ v, C )
refocus_{aux} (C [A [ ]], v) = (A v, C )

In this abstract machine, the configurations are pairs containing a closure and a context; the final transitions are specified by the first, third, and fifth clauses of refocus and by the first, third, and fourth clauses of refocus_{aux}; and the initial transition is specified by two clauses of the corresponding ‘refocused’ evaluation function, which reads as follows:

iterate : Value + (Redex × Context) → Value
iterate v = v
iterate (r, C ) = iterate (refocus (c′, C′))

where (c′, C′) = contract (r, C )

evaluate : Term → Value
evaluate t = iterate (refocus (t[•], [ ]))

(For the initial call to iterate, we have exploited the double equality decompose (t[•]) = decompose (plug (t[•], [ ])) = refocus (t[•], [ ]).)

This evaluation function computes the transitive closure of refocus using the auxiliary function iterate as a trampoline [48]. Due to the non-tail call to refocus in iterate, we refer to this evaluation function as a ‘pre-abstract machine.’

3.3 A staged abstract machine

To transform the pre-abstract machine into an abstract machine, we distribute the calls to iterate from the definitions of evaluate and of iterate to the definitions of refocus and refocus_{aux}:

evaluate : Term → Value
evaluate t = refocus (t[•], [ ])
iterate : Value + (Redex × Context) → Value
iterate v = v
iterate (r, C ) = refocus (c′, C′)

where (c′, C′) = contract (r, C )

refocus : Closure × Context → Value
refocus (i[s], C ) = iterate (i[s], C )
refocus ((λt)[s], C ) = refocus_{aux} (C , (λt)[s])
refocus ((t_{0} t_{1})[s], C ) = iterate ((t_{0} t_{1})[s], C )
refocus (c_{0} c_{1}, C ) = refocus (c_{0}, C [[ ] c_{1}])
refocus ((A t)[s], C ) = iterate ((A t)[s], C )
refocus (A c, C ) = refocus (c, C [A [ ]])
refocus_{aux} : Context × Value → Value
refocus_{aux} ([ ], v) = iterate v
refocus_{aux} (C [[ ] c], v) = refocus (c, C [v [ ]])
refocus_{aux} (C [v′ [ ]], v) = iterate (v′ v, C )
refocus_{aux} (C [A [ ]], v) = iterate (A v, C )

The resulting definitions of evaluate, iterate, refocus, and refocus_{aux} are that of four mutually recursive transition functions that form an abstract machine. In this abstract machine, the configurations are pairs of a closure and a context, the initial transition is specified by evaluate, and the final transition in the first clause of iterate. The compatibility rules are implemented by refocus and refocus_{aux}, and the reduction rules by the call to contract in the second clause of iterate. We can make this last point even more manifest by inlining contract in the definition of iterate:

iterate : Value + (Redex × Context) → Value
iterate v = v
iterate (i[v_{1} ⋯ v_{m}], C ) = refocus (v_{i}, C )
iterate ((t_{0} t_{1})[s], C ) = refocus ((t_{0}[s]) (t_{1}[s]), C )
iterate (((λt)[s]) v, C ) = refocus (t[v · s], C )
iterate ((A t)[s], C ) = refocus (A (t[s]), C )
iterate (A v, C ) = refocus (v, [ ])

By construction, the machine therefore separately implements the reduction rules (with iterate) and the compatibility rules (with refocus and refocus_{aux}); for this reason, we refer to it as a ‘staged abstract machine’ [51].

3.4 An eval/apply abstract machine

As already observed by Danvy and Nielsen in their work on refocusing, inlining iterate yields an eval/apply abstract machine [66]. Inlining the calls to iterate in the staged abstract machine yields the following eval/apply machine, where refocus (the ‘eval’ transition function) dispatches on closures and refocus_{aux} (the ‘apply’ function) dispatches on contexts:

evaluate : Term → Value
evaluate t = refocus (t[•], [ ])
refocus : Closure × Context → Value
refocus (i[v_{1} ⋯ v_{m}], C ) = refocus (v_{i}, C )
refocus ((λt)[s], C ) = refocus_{aux} (C , (λt)[s])
refocus ((t_{0} t_{1})[s], C ) = refocus ((t_{0}[s]) (t_{1}[s]), C )
refocus (c_{0} c_{1}, C ) = refocus (c_{0}, C [[ ] c_{1}])
refocus ((A t)[s], C ) = refocus (A (t[s]), C )
refocus (A c, C ) = refocus (c, C [A [ ]])
refocus_{aux} : Context × Value → Value
refocus_{aux} ([ ], v) = v
refocus_{aux} (C [[ ] c], v) = refocus (c, C [v [ ]])
refocus_{aux} (C [((λt)[s]) [ ]], v) = refocus (t[v · s], C )
refocus_{aux} (C [A [ ]], v) = refocus (v, [ ])

3.5 Transition compression

In three cases, the eval/apply machine of Section 3.4 yields a configuration that uniquely determines the next one. Let us shortcut these “corridor transitions:”

• The machine only produces an application of closures through an (App) reduction step (third clause of refocus). We observe that in a reduction sequence, an (App) reduction step is always followed by a decomposition step (fourth clause of refocus). As a shortcut, we coalesce the two consecutive transitions into one, replacing the third and fourth clauses of refocus with the following one:

refocus ((t_{0} t_{1})[s], C ) = refocus (t_{0}[s], C [[ ] (t_{1}[s])])

• The machine only produces an application of A through an (Abort) reduction step (second-to-last clause of refocus). We observe that in a reduction sequence, an (Abort) reduction step is always followed by a decomposition step (last clause of refocus). As a shortcut, we coalesce the two consecutive transitions into one, replacing the last two clauses of refocus with the following one:

refocus (A (t[s]), C ) = refocus (t[s], C [A [ ]])

• The configuration refocus (v, [ ]) always yields the configuration refocus_{aux} ([ ], v), which triggers a final transition. As a shortcut, we coalesce these three consecutive transitions into one final transition, replacing the last clause of refocus_{aux} with the following one:

refocus_{aux} (C [A [ ]], v) = v

3.6 An environment machine

Because of the two first compressions of Section 3.5, refocus is now defined by structural induction over terms instead of by structural induction over closures. Its type can therefore be refined to (Term×Substitution)×Context → Value+(Redex×Context), in effect unfolding closures into a term and a substitution. We thus replace each closure in the compressed definition of evaluate and refocus by its unfolding. Flattening (Term×Substitution)×Context into Term × Substitution × Context yields the following abstract machine:

(Value)  v ::= (λt, s)
(Context)  C ::= [ ] | C [[ ] (t, s)] | C [v [ ]] | C [A [ ]]
evaluate : Term → Value
evaluate t = refocus (t, •, [ ])
refocus : Term × Substitution × Context → Value
refocus (i, v_{1} ⋯ v_{m}, C ) = refocus (v_{i}, C )
refocus (λt, s, C ) = refocus_{aux} (C , (λt, s))
refocus (t_{0} t_{1}, s, C ) = refocus (t_{0}, s, C [[ ] (t_{1}, s)])
refocus (A t, s, C ) = refocus (t, s, C [A [ ]])
refocus_{aux} : Context × Value → Value
refocus_{aux} ([ ], v) = v
refocus_{aux} (C [[ ] (t, s)], v) = refocus (t, s, C [v [ ]])
refocus_{aux} (C [(λt, s) [ ]], v) = refocus (t, v · s, C )
refocus_{aux} (C [A [ ]], v) = v

We observe that this machine coincides with the CEK machine extended with an abort operator—an extension that was designed as such [42]. In particular, the substitution component assumes the role of the environment.

3.7 Correctness

We state the correctness of the final result—the CEK machine—with respect to evaluation in the λρ̂A-calculus.

Theorem 1. For any closed term t in λρ̂A,

t[•] →_{A}^{∗} (λt′)[s′] if and only if evaluate t = (λt′, s′).

Proof. The proof relies on the correctness of refocusing [36], and the (trivial) meaning preservation of each of the subsequent transformations.

The theorem states that the CEK machine is correct in the sense that it computes closed weak head normal forms, and that it realizes the applicative-order strategy in the λρ̂Acalculus, which makes it a call-by-value machine [70]. Furthermore, each of the intermediate abstract machines is also correct with respect to call-by-value evaluation in the λρ̂A-calculus.

3.8 Conclusion

We have presented a detailed and systematic derivation of an abstract machine for call-by-value evaluation in the λ-calculus with an abort operation. We started from the specification of the applicative-order reduction strategy in the λρ̂-calculus with an abort operation and we finished with a formal correspondence between the calculus and tbe abstract machine.

In the next six sections, we apply the same method in a variety of computational situations, each of which has been separately studied and reported in the literature. Our presentation is structured around four elements: language, notion of context-sensitive reduction, abstract machine, and formal correspondence. The rest is mechanical and therefore omitted.

4 The λρ̂K-calculus

The Krivine machine is probably the best-known abstract machine implementing the normal-order reduction strategy in the λ-calculus [30]. In our previous work [8], we have pointed out that Krivine’s original machine [59] does not coincide with the Krivine Machine As We Know It [21,23] in that it implements g\underline{eneralized} instead of \underline{ordinar}y β-reduction: indeed Krivine’s machine reduces the term (λλt) t_{1} t_{2} in one step whereas the Krivine machine reduces it in two steps. Furthermore, an extension of the archival version of Krivine’s machine [60, Section 3] also caters for call/cc (noted K below).

In our previous work [8], we have presented the calculus corresponding to the original version of Krivine’s machine. This machine uses closures and an environment and correspondingly, the calculus is one of explicit substitutions, λρ̂.

Here, we present the calculus corresponding to the archival version of Krivine’s machine with K. This machine also uses closures and an environment. Correspondingly, the calculus is one of explicit substitutions, λρ̂K. We build on top of Krivine’s language of terms by specifying syntactic categories of closures and substitutions as shown below. The calculus is tied to a particular reduction strategy. Here, like Krivine, we consider the normal-order reduction strategy and therefore call by name [70].

4.1 The language of λρ̂K

The abstract syntax of the language is as follows:

(terms)  t ::= i | λ^{n}t | t t | K t
(closures)  c ::= t[s] | c c | K c | ⌜C⌝
(values)  v ::= (λ^{n}t)[s] | ⌜C⌝
(substitutions)  s ::= • | c · s
(reduction contexts) C ::= [ ] | C [[ ] c] | C [K[ ]]

A nested λ-abstraction of the form λ^{n}t is to be understood as a syntactic abbreviation for \underbrace{λλ… λ}_{n} t, where t is not a λ-abstraction.

In λρ̂K, a value is either a closure with a λ-abstraction in the term part, or the representation of a reduction context captured by K.

4.2 Notion of context-sensitive reduction

The notion of reduction is specified by the set of rules shown below. The rules (Var) and (Prop) are as in the λρ̂-calculus, and (Beta^{+}) supersedes the (Beta) rule by performing a generalized β-reduction in one step:

(Var)  ⟨i[c_{1} ⋯ c_{j}], C ⟩ →_{K} ⟨c_{i}, C ⟩ if i ≤ j
(Beta^{+}) ⟨(λ^{n}t)[s], C [[… [[ ] c_{n}] …] c_{1}]⟩ →_{K} ⟨t[c_{1} ⋯ c_{n} · s], C ⟩
(Beta_{C} )  ⟨⌜C′⌝, C [[ ] c]⟩ →_{K} ⟨c, C′⟩

(Prop) ⟨(t_{0} t_{1})[s], C ⟩ →_{K} ⟨(t_{0}[s]) (t_{1}[s]), C ⟩
(Prop_{K}) ⟨(K t)[s], C ⟩ →_{K} ⟨K (t[s]), C ⟩
(K_{λ}) ⟨K ((λt)[s]), C ⟩ →_{K} ⟨t[⌜C⌝ · s], C ⟩
(K_{C} )  ⟨K ⌜C′⌝, C ⟩ →_{K} ⟨⌜C′⌝ ⌜C⌝, C ⟩

The three last rules account for call/cc: the first is an ordinary propagation rule, and the two others describe a continuation capture. In the first case, the current continuation is captured and passed to a function, and in the second, it is captured and passed to an already captured continuation.

4.3 Krivine’s machine

Refocusing, compressing the intermediate transitions, and unfolding the data type of closures mechanically yields the following environment-based machine:

⟨i, s, C ⟩ ⇒_{K} ⟨t′, s′, C ⟩ if s(i) = (t′, s′)
⟨i, s, C ⟩ ⇒_{K} ⟨C , ⌜C′⌝⟩ if s(i) = ⌜C′⌝
⟨λ^{n}t, s, C ⟩ ⇒_{K} ⟨C , (λ^{n}t, s)⟩
⟨t_{0} t_{1}, s, C ⟩ ⇒_{K} ⟨t_{0}, s, C [[ ] (t_{1}, s)]⟩
⟨K t, s, C ⟩ ⇒_{K} ⟨t, s, C [K[ ]]⟩
⟨[ ], v⟩ ⇒_{K} v
⟨C [[… [[ ] c_{n}] …] c_{1}], (λ^{n}t, s)⟩ ⇒_{K} ⟨t, c_{1} ⋯ c_{n} · s, C ⟩
⟨C [[ ] (t, s)], ⌜C′⌝⟩ ⇒_{K} ⟨t, s, C′⟩
⟨C [[ ] ⌜C′′⌝], ⌜C′⌝⟩ ⇒_{K} ⟨C′, ⌜C′′⌝⟩
⟨C [K[ ]], v⟩ ⇒_{K} ⟨C [[ ] ⌜C⌝], v⟩

This machine coincides with the extension of Krivine’s machine with K—an extension which was designed as such and not connected to any calculus [60, Section 3].

4.4 Formal correspondence

Proposition 4. For any term t in the λρ̂K-calculus,

t[•] →_{K}^{∗} v if and only if ⟨t, •, [ ]⟩ ⇒_{K}^{∗} v.

The λρ̂K-calculus therefore directly corresponds to the archival version of Krivine’s machine with call/cc.

5 The λρ̂μ-calculus

In this section we present a calculus of closures that extends Parigot’s λμ-calculus [69] and the corresponding call-by-name abstract machine obtained by refocusing.

We want to compare our derived abstract machine with an existing one designed by de Groote [38] and therefore we adapt his syntax, which differs from Parigot’s in that arbitrary terms can be abstracted by μ (not only named ones). In addition, de Groote presents a calculus of explicit substitutions built on top of the λμ-calculus, and uses it to prove the correctness of his machine. We show that a λρ̂-like calculus of closures is enough to model evaluation in the λμ-calculus and to derive the same abstract machine as de Groote.

The λμ-calculus is typed, and suitable typing rules can be given to the calculus of closures we present below. The reduction rules we show satisfy the subject reduction property, and in consequence, the machine we derive operates on typed terms. To remain concise, we omit all the typing considerations and concentrate on the syntactic correspondence between the calculus and the machine.

5.1 The language of λρ̂μ

We use de Bruijn indices for both the λ-bound variables and the μ-bound variables. The two kinds of variables are represented using the same set of indices, which leads one to an abstract machine with one environment [38]. Alternatively, we could use two separate sets of indices, which would then yield two environments in the resulting machine (one for each kind of variable).

The abstract syntax of the language is specified as follows:

(terms)  t ::= i | λt | t t | μt | [i]t
(closures)  c ::= t[s] | c c
(values)  v ::= (λt)[s]
(substitutions)  s ::= • | C · s | c · s
(reduction contexts) C ::= [ ] | C [[ ] c]

We consider only closed λ-terms, and i ≥ 0. Bound variables are indexed starting with 1, and a (free) occurrence of a variable 0 indicates a distinguished toplevel continuation (similar to tp in Ariola et al.’s setting [6]). A substitution is a non-empty sequence of either closures—to be substituted for λ-bound variables, or captured reduction contexts—to be used when accessing μ-bound variables.

Programs are closures of the form t[[ ] · •], where the empty context is to be substituted for the toplevel continuation variable 0.

5.2 Notion of context-sensitive reduction

The notion of reduction extends that of the λρ̂ with two rules: (Mu), which captures the entire reduction context and stores it in the substitution, and (Rho), which reinstates a captured context when a continuation variable is applied:

(Beta)  ⟨(λt)[s], C [[ ] c]⟩ →_{μ} ⟨t[c · s], C ⟩
(Var)  ⟨i[s], C ⟩ →_{μ} ⟨c, C ⟩ if s(i) = c
(Prop)  ⟨(t_{0} t_{1})[s], C ⟩ →_{μ} ⟨(t_{0}[s]) (t_{1}[s]), C ⟩
(Mu)  ⟨(μt)[s], C ⟩ →_{μ} ⟨t[C · s], [ ]⟩
(Rho)  ⟨([i]t)[s], [ ]⟩ →_{μ} ⟨t[s], C ⟩ if s(i) = C

5.3 An eval/apply abstract machine

Refocusing, compressing the intermediate transitions, and unfolding the data type of closures mechanically yields the following environment-based machine:

⟨λt, s, C ⟩ ⇒_{μ} ⟨C , (λt, s)⟩
⟨i, s, C ⟩ ⇒_{μ} ⟨t′, s′, C ⟩ if s(i) = (t′, s′)
⟨t_{0} t_{1}, s, C ⟩ ⇒_{μ} ⟨t_{0}, s, C [[ ] (t_{1}, s)]⟩
⟨μt, s, C ⟩ ⇒_{μ} ⟨t, C · s, [ ]⟩
⟨[i]t, s, [ ]⟩ ⇒_{μ} ⟨t, s, C ⟩ if s(i) = C

\begin{aligned}⟨[ ], v⟩ & ⇒_{μ} & v \\ ⟨C [[ ] c], (λt, s)⟩ & ⇒_{μ} & ⟨t, c · s, C ⟩ \end{aligned}

This machine coincides with de Groote’s final abstract machine [38, p. 24], except that instead of traversing the environment as a list, it directly fetches the right substitutee for a given index i.

5.4 Formal correspondence

Proposition 5. For any term t in the λρ̂μ-calculus,

t[[ ] · •] →_{μ}^{∗} v if and only if ⟨t, [ ] · •, [ ]⟩ ⇒_{μ}^{∗} v.

The λρ̂μ-calculus therefore directly corresponds to de Groote’s abstract machine for the λμ-calculus.

6 Delimited continuations

Continuations have been discovered multiple times [73], but they acquired their name for describing jumps [82], using what is now known as continuation-passing style (CPS) [80]. A full-fledged control operator, J [62,84], however, existed before CPS, providing first-class continuations in direct style. Continuations therefore existed before CPS, and so one could say that it was really CPS that was discovered multiple times.

Conversely, delimited continuations, in the form of the traditional success and failure continuations [76], have been regularly used in artificial-intelligence programming [14, 54, 83] for generators and backtracking. They also occur in the study of reflective towers [79], where the notions of meta-continuation [89] and of “jumpy” vs. “pushy” continuations [34] arose. A full-fledged delimited control operator, # (pronounced “prompt”), however, was introduced independently of CPS and of reflective towers, to support operational equivalence in λ-calculi with first-class control [41, 44]. Only subsequently were control delimiters connected to success and failure continuations [32].

The goal of this section is to provide a uniform account of delimited continuations. Three data points are in presence—a calculus and an abstract machine, both invented by Felleisen [41], and an extension of CPS, as discovered by Danvy and Filinski [32]:

Calculus: As we show below, an explicit-substitutions version of Felleisen’s calculus of dynamic delimited continuations can be refocused into his extension of the CEK machine, which uses closures and an environment.

Abstract machine: As we have shown elsewhere [11], Felleisen’s extension of the CEK machine is not in defunctionalized form (at least for the usual notion of defunctionalization [35, 72]); it needs some adjustment to be so, which leads one to a dynamic form of CPS that threads a state-like trail of delimited contexts.

CPS: Defunctionalizing Danvy and Filinski’s continuation-based evaluator yields an environment-based machine [7], and we present below the corresponding calculus of static delimited continuations.

The syntactic correspondence makes it possible to directly compare (1) the calculi of dynamic and of static delimited continuations, (2) the extended CEK machine and the machine corresponding to the calculus of static delimited continuations and to the continuation-based evaluator, and (3) the evaluator corresponding to the extended CEK machine and the continuation-based evaluator. In other words, rather than having to relate heterogeneous semantic artifacts such as a calculus with actual substitutions, an environment-based machine, and a continuation-based evaluator, we are now in position to directly compare two calculi, two abstract machines, and two continuation-based evaluators.

We address static delimited continuations in Section 6.1 and dynamic delimited continuations in Section 6.2. In both cases, we consider the left-to-right applicative-order reduction strategy and therefore left-to-right call by value.

6.1 The λρ̂S-calculus

The standard λ-calculus is extended with the control operator shift (written S) that captures the current delimited continuation and with the control delimiter reset (written ⟨⟨⟨·⟩⟩⟩) that initializes the current delimited continuation.

6.1.1 The language of λρ̂S

The abstract syntax of the language is as follows:

(terms)  t ::= i | λt | t t | S t | ⟨⟨⟨t⟩⟩⟩
(closures)  c ::= t[s] | c c | S c | ⟨⟨⟨c⟩⟩⟩ | ⌜C⌝
(values)  v ::= (λt)[s] | ⌜C⌝
(substitutions)  s ::= • | c · s
(contexts)  C_{1} ::= [ ] | C_{1}[v [ ]] | C_{1}[[ ] c] | C_{1}[S[ ]]
(meta-contexts) C_{2} ::= • | C_{1} · C_{2}

For readability, we write C_{1} · C_{2} rather than C_{2}[⟨⟨⟨C_{1}[ ]⟩⟩⟩].

The control operator S captures the current delimited context and replaces it with the empty context. The control delimiter ⟨⟨⟨·⟩⟩⟩ initializes the current delimited context, saving the then-current one onto the meta-context. When a captured delimited context is resumed, the current delimited context is saved onto the meta-context. When the current delimited context completes, the previously saved one, if there is any, is resumed; otherwise, the computation terminates. This informal description paraphrases the definitional interpreter for shift and reset, which has two layers of control—a current delimited continuation (akin to a success continuation) and a meta-continuation (akin to a failure continuation), as arises naturally when one CPS-transforms a direct-style evaluator twice [32]. Elsewhere [7], we have defunctionalized this interpreter into an environment-based machine, which we present next.

6.1.2 The eval/apply/meta-apply abstract machine

The environment-based machine is in “eval/apply/meta-apply” form (to build on Peyton Jones’s terminology [66]) because the continuation is defunctionalized into a context and the corresponding apply transition function, and the meta-continuation is defunctionalized into a meta-context (here a list of contexts) and the corresponding meta-apply transition function:

⟨i, s, C_{1}, C_{2}⟩ ⇒_{S} ⟨t′, s′, C_{1}, C_{2}⟩ if s(i) = (t′, s′)
⟨λt, s, C_{1}, C_{2}⟩ ⇒_{S} ⟨C_{1}, (λt, s), C_{2}⟩
⟨t_{0} t_{1}, s, C_{1}, C_{2}⟩ ⇒_{S} ⟨t_{0}, s, C_{1}[[ ] (t_{1}, s)], C_{2}⟩
⟨S t, s, C_{1}, C_{2}⟩ ⇒_{S} ⟨t, s, C_{1}[S[ ]], C_{2}⟩
⟨⟨⟨⟨t⟩⟩⟩, s, C_{1}, C_{2}⟩ ⇒_{S} ⟨t, s, [ ], C_{1} · C_{2}⟩

⟨[ ], v, C_{2}⟩ ⇒_{S} ⟨C_{2}, v⟩
⟨C_{1}[[ ] (t, s)], v, C_{2}⟩ ⇒_{S} ⟨t, s, C_{1}[v [ ]], C_{2}⟩
⟨C_{1}[(λt, s) [ ]], v, C_{2}⟩ ⇒_{S} ⟨t, v · s, C_{1}, C_{2}⟩
⟨C_{1}[⌜C′_{1}⌝ [ ]], v, C_{2}⟩ ⇒_{S} ⟨C′_{1}, v, C_{1} · C_{2}⟩
⟨C_{1}[S[ ]], (λt, s), C_{2}⟩ ⇒_{S} ⟨t, ⌜C_{1}⌝ · s, [ ], C_{2}⟩
⟨C_{1}[S[ ]], ⌜C′_{1}⌝, C_{2}⟩ ⇒_{S} ⟨C′_{1}, ⌜C_{1}⌝, [ ] · C_{2}⟩
⟨•, v⟩ ⇒_{S} v
⟨C_{1} · C_{2}, v⟩ ⇒_{S} ⟨C_{1}, v, C_{2}⟩

We have observed that this machine is in the range of refocusing, transition compression, and closure unfolding for the following calculus λρ̂S.

6.1.3 Notion of context-sensitive reduction

The λρ̂S-calculus uses two layers of contexts: C_{1} and C_{2}. A non-value closure is decomposed into a redex, a context C_{1}, and a meta-context C_{2}, and the notion of reduction is specified by the following rules:

(Var)  ⟨i[c_{1} ⋯ c_{j}], C_{1}, C_{2}⟩ →_{S} ⟨c_{i}, C_{1}, C_{2}⟩ if i ≤ j
(Beta)  ⟨((λt)[s]) v, C_{1}, C_{2}⟩ →_{S} ⟨t[v · s], C_{1}, C_{2}⟩
(Beta_{C} )  ⟨⌜C′_{1}⌝v , C_{1}, C_{2}⟩ →_{S} ⟨⟨⟨⟨C′_{1}[v]⟩⟩⟩, C_{1}, C_{2}⟩
(Prop)  ⟨(t_{0} t_{1})[s], C_{1}, C_{2}⟩ →_{S} ⟨(t_{0}[s]) (t_{1}[s]), C_{1}, C_{2}⟩
(Prop_{S})  ⟨(S t)[s], C_{1}, C_{2}⟩ →_{S} ⟨S (t[s]), C_{1}, C_{2}⟩
(Prop_{⟨⟨⟨·⟩⟩⟩})  ⟨⟨⟨⟨t⟩⟩⟩[s], C_{1}, C_{2}⟩ →_{S} ⟨⟨⟨⟨t[s]⟩⟩⟩, C_{1}, C_{2}⟩
(S_{λ})  ⟨S ((λt)[s]), C_{1}, C_{2}⟩ →_{S} ⟨t[⌜C_{1}⌝ · s], [ ], C_{2}⟩
(S_{C} )  ⟨S ⌜C′_{1}⌝, C_{1}, C_{2}⟩ →_{S} ⟨⌜C′_{1}⌝ ⌜C_{1}⌝, [ ], C_{2}⟩
(Reset)  ⟨⟨⟨⟨v⟩⟩⟩, C_{1}, C_{2}⟩ →_{S} ⟨v, C_{1}, C_{2}⟩

Since none of the contractions depends on the meta-context, it is evident that the notion of reduction →_{S} is compatible with meta-contexts, but it is not compatible with contexts, due to S_{λ} and S_{C} . The ⟨⟨⟨·⟩⟩⟩ construct therefore delimits the parts of non-value closures in which context-sensitive reductions may occur, and partially restores the compatibility of reductions. In particular, ⟨⟨⟨⟨t[s]⟩⟩⟩, C_{1}, C_{2}⟩ is decomposed into ⟨t[s], [], C_{1} ·C_{2}⟩ in the course of decomposition towards a context-sensitive redex.

6.1.4 Formal correspondence

Proposition 6. For any term t in the λρ̂S-calculus,

t[•] →_{S}^{∗} v if and only if ⟨t, •, [ ], •⟩ ⇒_{S}^{∗} v.

The λρ̂S-calculus therefore directly corresponds to the abstract machine for shift and reset.

6.1.5 The CPS hierarchy

Iterating the CPS transformation on a direct-style evaluator for the λ-calculus gives rise to a family of CPS evaluators. At each iteration, one can add shift and reset to the new inner layer. The result forms a CPS hierarchy of static delimited continuations [32, 37] which Filinski has shown to be able to represent layered monads [46]. Recently, Kameyama has proposed an axiomatization of the CPS hierarchy [56]. Elsewhere [7], we have studied its defunctionalized counterpart and the corresponding hierarchy of calculi.

6.2 The λρ̂F-calculus

The standard λ-calculus is extended with the control operator F that captures a segment of the current context and with the control delimiter prompt (noted #) that initializes a new segment in the current context.

6.2.1 The language of λρ̂F

The abstract syntax of the language is as follows:

(terms)  t ::= i | λt | t t | F t | #t
(closures)  c ::= t[s] | c c | F c | # c | ⌜C⌝
(values)  v ::= (λt)[s] | ⌜C⌝
(substitutions)  s ::= • | c · s
(reduction contexts) C ::= [ ] | C [[ ] c] | C [v [ ]] | C [F[ ]] | C [#[ ]]

6.2.2 Notion of context-sensitive reduction

The control operator F captures a segment of the current context up to a mark. The control delimiter # sets a mark on the current context. When a captured segment is resumed, it is composed with the current context. For the rest, the notion of reduction is as usual:^{2}

(Var)  ⟨i[c_{1} ⋯ c_{j}], C ⟩ →_{F} ⟨c_{i}, C ⟩ if i ≤ j
(Beta)  ⟨((λt)[s]) v, C ⟩ →_{F} ⟨t[v · s], C ⟩
(Beta_{C} )  ⟨⌜C′⌝v , C ⟩ →_{F} ⟨C′[v], C ⟩
(Prop)  ⟨(t_{0} t_{1})[s], C ⟩ →_{F} ⟨(t_{0}[s]) (t_{1}[s]), C ⟩
(Prop_{F})  ⟨(F t)[s], C ⟩ →_{F} ⟨F (t[s]), C ⟩
(Prop_{#})  ⟨(#t)[s], C ⟩ →_{F} ⟨# (t[s]), C ⟩
(F_{λ})  ⟨F ((λt)[s]), C [# C′]⟩ →_{F} ⟨t[⌜C′⌝ · s], C ⟩

if C′ contains no mark

(F_{C} )  ⟨F ⌜C′′⌝, C [# C′]⟩ →_{F} ⟨⌜C′′⌝ ⌜C′⌝, C ⟩

if C′ contains no mark

(Prompt)  ⟨# v, C ⟩ →_{F} ⟨v, C ⟩

Alternatively, we could specify the reduction rules using two layers of contexts, similarly to the λρ̂S-calculus [7, 10, 11]. The difference between the two calculi would then be only in the rule (Beta_{C} ):

(Beta_{C} ) ⟨⌜C′_{1}⌝v , C_{1}, C_{2}⟩ →_{F} ⟨C′_{1}[v], C_{1}, C_{2}⟩

where there is no delimiter around C′[v]. As in the previous case of the λρ̂S-calculus, such two-layered decomposition makes it evident that the contraction rules are compatible with the meta-context, since it is isolated by the use of a control delimiter.

2The original version of F does not reduce its argument first, but its followers do. The present version of F does likewise here, for a more direct comparison with S.

6.2.3 The eval/apply abstract machine

Refocusing, compressing the intermediate transitions, and unfolding the data type of closures mechanically yields the following environment-based machine:

⟨i, s, C ⟩ ⇒_{F} ⟨t′, s′, C ⟩ if s(i) = (t′, s′)
⟨λt, s, C ⟩ ⇒_{F} ⟨C , (λt, s)⟩
⟨t_{0} t_{1}, s, C ⟩ ⇒_{F} ⟨t_{0}, s, C [[ ] (t_{1}, s)]⟩
⟨F t, s, C ⟩ ⇒_{F} ⟨t, s, C [F[ ]]⟩
⟨#t, s, C ⟩ ⇒_{F} ⟨t, s, C [#[ ]]⟩
⟨C [[ ] (t, s)], v⟩ ⇒_{F} ⟨t, s, C [v [ ]]⟩
⟨C [(λt, s) [ ]], v⟩ ⇒_{F} ⟨t, v · s, C ⟩
⟨C [⌜C′⌝ [ ]], v⟩ ⇒_{F} ⟨C′ ∘ C , v⟩
⟨C [#C′[F[ ]]], (λt, s)⟩ ⇒_{F} ⟨t, ⌜C′⌝ · s, C ⟩

where C′ contains no mark

⟨C [#C′[F[ ]]], ⌜C′′⌝⟩ ⇒_{F} ⟨C′′ ∘ C , ⌜C′⌝⟩

where C′ contains no mark

⟨C [#[ ]], v⟩ ⇒_{F} ⟨C , v⟩

This machine coincides with Felleisen’s extension of the CEK machine—an extension which was designed as such [41, Section 3].

6.2.4 Formal correspondence

Proposition 7. For any term t in the λρ̂F-calculus,

t[•] →_{F}^{∗} v if and only if ⟨t, •, [ ]⟩ ⇒_{F}^{∗} v.

This proposition parallels Felleisen’s second correspondence theorem [41, p. 186]. The λρ̂F-calculus therefore directly corresponds to Felleisen’s extension of the CEK machine.

6.2.5 A hierarchy of control delimiters

As described by Sitaram and Felleisen [78], one could have not one but several marks in the context and have control operators capture segments of the current context up to a particular mark. For these marks not to interfere in programming practice, they need to be organized hierarchically, forming a hierarchy of control delimiters [78, Section 5]. Alternatively, one could iterate Biernacki et al.’s dynamic CPS transformation [11] to give rise to a hierarchy of dynamic delimited continuations with a functional (CPS) counterpart. Except for the work of Gunter et al. [50] and more recently of Dybvig et al. [39], this area is little explored.

6.3 Conclusion

The syntactic correspondence has made it possible to exhibit the calculus corresponding to static delimited continuations as embodied in the functional idiom of success and failure continuations and more generally in the CPS hierarchy, and to show that (the explicit-substitutions version of) Felleisen’s calculus of dynamic delimited continuations corresponds to his extension of the CEK machine [41]. Elsewhere, we present the abstract machine [7] and the evaluator [32] corresponding to static delimited continuations and an evaluator [11] corresponding to dynamic delimited continuations. We are now in position to compare them pointwise:

• From a calculus point of view, it seems to us that one is better off with layered contexts because it is immediately obvious whether a notion of reduction is compatible with them (see Section 6.1.3); a context containing marks is less easy to treat. Otherwise, the difference between static and dynamic delimited continuations is tiny (see Section 6.2.2), and located in the rule (Beta_{C} ).

• From a machine point of view, separating between the current delimited context and the other ones is also simpler, as it avoids linear searches, copies, and concatenations (in this respect, efficient implementations, e.g., with an Algol-style display, in effect separate between the current delimited context and the other ones).

• From the point of view of CPS, the abstract machine for dynamic delimited continuations is not in defunctionalized form whereas the abstract machine for static delimited continuations is (and corresponds to a evaluator in CPS). Conversely, defunctionalizing a CPS evaluator provides design guidelines, whereas without CPS, one is on one’s own, and locally plausible choices may have unforeseen global consequences which are then taken as the norm. Two cases in point:

1. in Lisp, it was locally plausible to push both formal and actual parameters at function-call time, and to pop them at return time, but this led to dynamic scope since variable lookup then follows the dynamic link; and

2. here, it was locally plausible to concatenate a control-stack segment to the current control stack (“From this, we learn that an empty context adds no information.” [45, p. 58]), but this led to dynamic delimited continuations since capturing a segment of a concatenated context then gives access to beyond the concatenation point.

Granted, a degree of dynamism makes it possible to write compact programs (e.g., a compositional breadth-first traversal without a data-queue accumulator and in direct style [12]), but it is very difficult to reason about them and they are not necessarily more efficient.

• From the point of view of expressiveness, for example, in Lisp, one can simulate the static scope of Scheme by making each lambda-abstraction a “funarg” and in Scheme, one can simulate the dynamic scope of Lisp by threading an environment of fluid variables in a state-monad fashion. Similarly, static delimited continuations can be simulated using dynamic ones by delimiting the extent of each captured continuation [10], and dynamic delimited continuations can be simulated using static ones by threading a trail of contexts in a state-monad fashion [11, 39, 58, 77]. As to which should be used by default, the question then reduces to which behavior is the norm and which should be simulated if it is needed.

In summary, the calculi, the abstract machines, and the evaluators all differ. In one approach, continuations are dynamically composed by concatenating their representations [45] and in the other, continuations are statically composed through a metacontinuation. These differences result from distinct designs: Felleisen and his colleagues started from a calculus and wanted to go “beyond continuations” [44], and therefore beyond CPS, whereas Danvy and Filinski were aiming at a CPS account of delimited control, one that has turned out to be not without practical, semantical, and logical content.

7 Stack inspection

This section addresses Fournet and Gordon’s λ_{sec}-calculus, which formalizes security enforcement by stack inspection [47]. We first present a calculus of closures built on top of the λ_{sec}-calculus, and we construct the corresponding environment-based machine. This machine is a storeless version of the fg machine presented by Clements and Felleisen [16, Figure 1]. (We consider the issue of store-based machines in Section 8.) This machine is not properly tail-recursive, and so Clements and Felleisen presented another machine—the cm machine—which does implement stack inspection in a properly tail-recursive manner [16, Figure 2]. The cm machine builds on Clinger’s formalization of proper tail-recursion (see Section 8) and it is therefore store-based; we considered its storeless version here, and we present the corresponding calculus of closures. We show how the tail-optimization of the cm machine is reflected in the calculus. Finally, we turn to the unzipped version of the cm machine [4] and we present the corresponding state-based calculus of closures.

7.1 The λρ̂_{sec}-calculus

7.1.1 The language of λρ̂_{sec}

(terms)  t ::= i | λt | t t | grant R in t | test R then t else t | R[t] | fail
(closures)  c ::= t[s] | c c | grant R in c | test R then c else c | R[c]
(values)  v ::= (λt)[s] | fail
(substitutions)  s ::= • | c · s
(reduction contexts) C ::= [ ] | C [[ ] c] | C [v [ ]] | C [grant R in [ ]] | C [R[[ ]]]
(permissions)  R ⊆ P

The set of terms consists of λ-terms and four constructs for handling different levels of security specified in a set P: grant R in t grants the permissions R to t; test R then t_{0} else t_{1} proceeds to evaluate t_{0} if permissions R are available, and otherwise t_{1}; a frame R[t] restricts the permissions of t to R; and finally, fail aborts the computation.

7.1.2 Notion of context-sensitive reduction

Given the predicate OK_{sec}(R, C ) checking whether the permissions R are available within the context C ,

\overline{OK_{sec}(∅, C )}  \overline{OK_{sec}(R, [ ])}

\frac{OK_{sec}(R, C )}{OK_{sec}(R, C [[ ] c])}  \frac{OK_{sec}(R, C )}{OK_{sec}(R, C [v [ ]])}

\frac{R ⊂ R′ OK_{sec}(R, C )}{OK_{sec}(R, C [R′[[ ]]])}  \frac{OK_{sec}(R \ R′, C )}{OK_{sec}(R, C [grant R′ in [ ]])}

the notion of reduction is given by the following set of rules:

(Var)  ⟨i[v_{1} ⋯ v_{j}], C ⟩ →_{sec} ⟨v_{i}, C ⟩ if i ≤ j
(Beta)  ⟨((λt)[s]) v, C ⟩ →_{sec} ⟨t[v · s], C ⟩
(Prop)  ⟨(t_{0} t_{1})[s], C ⟩ →_{sec} ⟨(t_{0}[s]) (t_{1}[s]), C ⟩
(Prop_{G}) ⟨(grant R in t)[s], C ⟩ →_{sec} ⟨grant R in t[s], C ⟩
(Prop_{F})  ⟨(R[t])[s], C ⟩ →_{sec} ⟨R[t[s]], C ⟩

(Prop_{T}) ⟨(test R then t_{0} else t_{1})[s], C ⟩ →_{sec} ⟨test R then t_{0}[s] else t_{1}[s], C ⟩
(Frame)  ⟨R[v], C ⟩ →_{sec} ⟨v, C ⟩
(Grant)  ⟨grant R in v, C ⟩ →_{sec} ⟨v, C ⟩
(Test_{1})  ⟨test R then c_{1} else c_{2}, C ⟩ →_{sec} ⟨c_{1}, C ⟩ if OK_{sec}(R, C )
(Test_{2})  ⟨test R then c_{1} else c_{2}, C ⟩ →_{sec} ⟨c_{2}, C ⟩ otherwise
(Fail)  ⟨fail[s], C ⟩ →_{sec} ⟨fail, [ ]⟩

The only context-sensitive rules are (Test_{1}) and (Test_{2}), which perform a reduction step after inspecting the entire context C , and (Fail) which aborts the computation.

7.1.3 An eval/apply abstract machine

Refocusing, compressing the intermediate transitions, and unfolding the data type of closures mechanically yields the following environment-based machine:

⟨i, s, C ⟩ ⇒_{sec} ⟨C , s(i)⟩
⟨λt, s, C ⟩ ⇒_{sec} ⟨C , (λt, s)⟩
⟨t_{0} t_{1}, s, C ⟩ ⇒_{sec} ⟨t_{0}, s, C [[ ] (t_{1}, s)]⟩
⟨grant R in t, s, C ⟩ ⇒_{sec} ⟨t, s, C [grant R in [ ]]⟩
⟨test R then t_{0} else t_{1}, s, C ⟩ ⇒_{sec} ⟨t_{0}, s, C ⟩ if OK_{sec}(R, C )
⟨test R then t_{0} else t_{1}, s, C ⟩ ⇒_{sec} ⟨t_{1}, s, C ⟩ otherwise
⟨fail, s, C ⟩ ⇒_{sec} fail
⟨R[t], s, C ⟩ ⇒_{sec} ⟨t, s, C [R[[ ]]]⟩
⟨[ ], v⟩ ⇒_{sec} v
⟨C [[ ] (t, s)], v⟩ ⇒_{sec} ⟨t, s, C [v [ ]]⟩
⟨C [(λt, s) [ ]], v⟩ ⇒_{sec} ⟨t, v · s, C ⟩
⟨C [grant R in [ ]], v⟩ ⇒_{sec} ⟨C , v⟩
⟨C [R[[ ]]], v⟩ ⇒_{sec} ⟨C , v⟩

This machine is a storeless version of Clements and Felleisen’s fg machine [16, Figure 1].

7.1.4 Formal correspondence

Proposition 8. For any term t in the λρ̂_{sec}-calculus,

t[•] →_{sec}^{∗} v if and only if ⟨t, •, [ ]⟩ ⇒_{sec}^{∗} v.

The λρ̂_{sec}-calculus therefore directly corresponds to the storeless version of the fg machine.

7.2 Properly tail-recursive stack inspection

On the ground that the fg machine is not properly tail-recursive, Clements and Felleisen presented a new, properly tail-recursive, machine—the cm machine [16, Figure 2]—thereby debunking the folklore that stack inspection is incompatible with proper tail recursion. Below, we consider the storeless version of the cm machine and we present the underlying calculus of closures.

7.2.1 The storeless cm machine

The cm machine operates on a λ_{sec}-term, an environment, and an evaluation context enriched with updatable permission tables (written m below):

(stack frames) C ::= m[ ] | C [[ ](c, m)] | C [(v, m)[ ]]

A permission table is a partial function with a finite domain from a set of permissions P to the set {⊥ = not granted, ⊤ = granted}. A permission table with the empty domain is written ε.

Given the predicate OK_{sec}^{cm}(R, C ),

\overline{OK_{sec}^{cm}(∅, C )} \frac{R ∩ m^{−1}(⊥) = ∅}{OK_{sec}^{cm}(R, m[ ])}

\frac{R ∩ m^{−1}(⊥) = ∅ OK_{sec}^{cm}(R \ m^{−1}(⊤), C )}{OK_{sec}^{cm}(R, C [[ ](c, m)])} \frac{R ∩ m^{−1}(⊥) = ∅ OK_{sec}^{cm}(R \ m^{−1}(⊤), C )}{OK_{sec}^{cm}(R, C [(v, m)[ ]])}

the transitions of the storeless cm machine read as follows:

⟨i, s, C ⟩ ⇒_{sec}^{cm} ⟨C , s(i)⟩
⟨λt, s, C ⟩ ⇒_{sec}^{cm} ⟨C , (λt, s)⟩
⟨t_{0} t_{1}, s, C ⟩ ⇒_{sec}^{cm} ⟨t_{0}, s, C [[ ]((t_{1}, s), ε)]⟩
⟨grant R in t, s, C ⟩ ⇒_{sec}^{cm} ⟨t, s, C [R ↦ ⊤]⟩
⟨test R then t_{0} else t_{1}, s, C ⟩ ⇒_{sec}^{cm} ⟨t_{0}, s, C ⟩ if OK_{sec}^{cm}(R, C )
⟨test R then t_{0} else t_{1}, s, C ⟩ ⇒_{sec}^{cm} ⟨t_{1}, s, C ⟩ otherwise
⟨fail, s, C ⟩ ⇒_{sec}^{cm} fail
⟨R[t], s, C ⟩ ⇒_{sec}^{cm} ⟨t, s, C [\overline{R} ↦ ⊥]⟩
⟨m[ ], v⟩ ⇒_{sec}^{cm} v
⟨C [[ ]((t, s), m)], v⟩ ⇒_{sec}^{cm} ⟨t, s, C [(v, ε)[ ]]⟩
⟨C [((λt, s), m)[ ]], v⟩ ⇒_{sec}^{cm} ⟨t, v · s, C ⟩

where \overline{R} = P \ R and C [R ↦ v] is a modification of the permission table in the context C obtained by granting or restricting the permissions R, depending on v.

The following proposition states the equivalence of the fg machine and the cm machine with respect to the values they compute:

Proposition 9. For any term t in the λρ̂_{sec}-calculus,

⟨t, •, [ ]⟩ ⇒_{sec}^{∗} v if and only if ⟨t, •, [ ]⟩ (⇒_{sec}^{cm})^{∗} v.

Moreover, it can be shown that each step of the fg machine is simulated by at most one step of the cm machine [16]. At the level of the calculus, this is reflected in the fact that the reduction semantics implemented by the cm machine has fewer reductions than λρ̂_{sec}.

7.2.2 The underlying calculus λρ_{sec}^{cm}

The calculus corresponding to the storeless cm machine is very close to the λρ̂_{sec}-calculus. The grammar of terms, closures and substitutions is the same, but the reduction contexts (which correspond to the stack frames in the machine) contain permission tables.

Consequently, the functions plug and decompose are defined in a non-standard way:

plug (c, m[ ])  = build (m, c)
plug (c_{0}, C [[ ](c_{1}, m)]) = plug (build (m, c_{0} c_{1}), C )
plug (c, C [(v, m)[ ]]) = plug (build (m, v c), C )

where the auxiliary function build conservatively constructs a closure based on the permission table of the reduction context:

build_{G} (m, c) = \begin{cases}c & if m^{−1}(⊤) = ∅ \\ grant m^{−1}(⊤) in c & otherwise \end{cases}
build_{F} (m, c) = \begin{cases}c & if m^{−1}(⊥) = ∅ \\ \overline{m^{−1}(⊥)}[c] & otherwise \end{cases}
build (m, c) = build_{F} (m, build_{G} (m, c))

Any closure that is not already a value or a potential redex, can be further decomposed as follows:

decompose (c_{0} c_{1}, C )  = decompose (c_{0}, C [[ ](c_{1}, ε)])
decompose (grant R in c, C ) = decompose (c, C [R ↦ ⊤])
decompose (R[c], C )  = decompose (c, C [\overline{R} ↦ ⊥])
decompose (v, C [[ ](c, m)]) = decompose (c, C [(v, ε)[ ]])

The notion of reduction includes most rules of the λρ̂_{sec}-calculus, except for (Frame) and (Grant).

From a calculus standpoint, Clements and Felleisen therefore obtained proper tail recursion by changing the computational model (witness the change from OK_{sec} to OK_{sec}^{cm}) and by simplifying the reduction rules and modifying the compatibility rules.

7.3 State-based properly tail-recursive stack inspection

On the observation that the stack of the cm machine can be unzipped into the usual control stack of the CEK machine and a state-like list of permission tables, Ager et al. have presented an unzipped version of the cm machine (characterizing properly tail-recursive stack inspection as a monad, in passing) [4]. We first present this machine, and then the corresponding calculus of closures.

7.3.1 The unzipped storeless cm machine

The unzipped cm machine operates on a λ_{sec}-term, an environment, and an ordinary evaluation context. In addition, the machine has a read-write security register m holding the current permission table and a read-only security register ms holding a list of outer permission tables. Given the predicate OK_{sec}^{ucm}(R, m, ms),

OK_{sec}^{ucm}(∅, m, ms)

\frac{R ∩ m^{−1}(⊥) = ∅}{OK_{sec}^{ucm}(R, m, •)} \frac{R ∩ m^{−1}(⊥) = ∅ OK_{sec}^{ucm}(R \ m^{−1}(⊤), m′, ms)}{OK_{sec}^{ucm}(R, m, m′ · ms)}

the transitions of the unzipped storeless cm machine read as follows:

⟨i, s, m, ms, C ⟩ ⇒_{sec}^{ucm} ⟨C , s(i), ms⟩
⟨λt, s, m, ms, C ⟩ ⇒_{sec}^{ucm} ⟨C , (λt, s), ms⟩
⟨t_{0} t_{1}, s, m, ms, C ⟩ ⇒_{sec}^{ucm} ⟨t_{0}, s, ε, m · ms, C [[ ] (t_{1}, s)]⟩

⟨grant R in t, s, m, ms, C ⟩ ⇒_{sec}^{ucm} ⟨t, s, m[R↦⊤], ms, C ⟩
⟨test R then t_{0} else t_{1}, s, m, ms, C ⟩ ⇒_{sec}^{ucm} ⟨t_{0}, s, m, ms, C ⟩ if OK_{sec}^{ucm}(R, m, ms)
⟨test R then t_{0} else t_{1}, s, m, ms, C ⟩ ⇒_{sec}^{ucm} ⟨t_{1}, s, m, ms, C ⟩ otherwise
⟨R[t], s, m, ms, C ⟩ ⇒_{sec}^{ucm} ⟨t, s, m[\overline{R}↦⊥], ms, C ⟩
⟨fail, s, m, ms, C ⟩ ⇒_{sec}^{ucm} fail
⟨[ ], v, •⟩ ⇒_{sec}^{ucm} v
⟨C [[ ] (t, s)], v, ms⟩ ⇒_{sec}^{ucm} ⟨t, s, ε, ms, C [v [ ]]⟩
⟨C [(λt, s) [ ]], v, m · ms⟩ ⇒_{sec}^{ucm} ⟨t, v · s, m, ms, C ⟩

The following proposition states the equivalence of the cm machine and the unzipped cm machine:

Proposition 10. For any term t in the λρ̂_{sec}-calculus,

⟨t, •, [ ]⟩ (⇒_{sec}^{cm})^{∗} v if and only if ⟨t, •, ε, •, [ ]⟩ (⇒_{sec}^{ucm})^{∗} v.

Moreover, it can be shown that each step of the cm machine is simulated by one step of the unzipped cm machine.

7.3.2 The language of λρ_{sec}^{ucm}

(terms)  t ::= i | λt | t t | grant R in t | test R then t else t | R[t] | fail
(closures)  c ::= t[s]
(values)  v ::= (λt)[s] | fail
(substitutions)  s ::= • | c · s
(reduction contexts) C ::= [ ] | C [[ ] c] | C [v [ ]]
(annotated closures) c̃::= c[m, ms] | c c̃ | c̃c | fail
(annotated values) ṽ ::= v[m, ms] | fail

7.3.3 Notion of context-sensitive reduction

The notion of reduction is specified by the rules below. Compared to the rules of Section 7.1.2, the current permission table and the list of outer permission tables are propagated locally to each closure being evaluated. When a value is consumed, the current permission table is discarded.

The (Prop) reduction rule illustrates the propagation to a subclosure to be evaluated:

⟨(t_{0} t_{1})[s][m, ms], C ⟩ →_{sec}^{ucm} ⟨(t_{0}[s][ε, m · ms]) (t_{1}[s]), C ⟩

So do half of the other reduction rules:

(Var)  ⟨i[c_{1} ⋯ c_{j}][m, ms], C ⟩ →_{sec}^{ucm} ⟨c_{i}[m, ms], C ⟩ if i ≤ j
(Test_{1}) ⟨(test R then t_{0} else t_{1})[s][m, ms], C ⟩ →_{sec}^{ucm} ⟨t_{0}[s][m, ms], C ⟩ if OK_{sec}^{ucm}(R, m, ms)
(Test_{2}) ⟨(test R then t_{0} else t_{1})[s][m, ms], C ⟩ →_{sec}^{ucm} ⟨t_{1}[s][m, ms], C ⟩ otherwise
(Fail)  ⟨fail[s][m, ms], C ⟩ →_{sec}^{ucm} ⟨fail, [ ]⟩

A new reduction rule, however, is now necessary to go from one evaluated subclosure to a subclosure to evaluate:

(Switch)  ⟨(v[m, ms]) c, C ⟩ →_{sec}^{ucm} ⟨v (c[ε, ms]), C ⟩

The (Beta) rule doubles up with discarding the permission table of the actual parameter:

(Beta) ⟨((λt)[s]) (v[m, m′ · ms]), C ⟩ →_{sec}^{ucm} ⟨t[v · s][m′, ms], C ⟩

Finally, the (Frame) and (Grant) rules embody the state counterpart of Clements and Felleisen’s design to enable proper tail recursion:

(Frame)  ⟨R[t][s][m, ms], C ⟩ →_{sec}^{ucm} ⟨t[s][m[\overline{R}↦⊥], ms], C ⟩
(Grant) ⟨(grant R in t)[s][m, ms], C ⟩ →_{sec}^{ucm} ⟨t[s][m[R↦⊤], ms], C ⟩

7.3.4 Formal correspondence

Proposition 11. For any term t in the λ_{sec}-calculus, t[•](→_{sec}^{ucm})^{∗}v if and only if ⟨t, •, ε, •, [ ]⟩ (⇒_{sec}^{ucm})^{∗} v.

7.4 Conclusion

We have presented three corresponding calculi of closures and machines for stack inspection, showing first how the storeless fg machine reflects the λρ̂_{sec}-calculus, second, how the λρ_{sec}^{cm}-calculus reflects the storeless cm machine, and third, how the λρ_{sec}^{ucm}-calculus reflects the unzipped storeless cm machine. In doing so, we have provided a calculus account of machine design and optimization for stack inspection.

8 A calculus for proper tail-recursion

At PLDI’98 [19], Clinger presented a properly tail-recursive semantics for Scheme in the form of a store-based abstract machine. This machine models the memory-allocation behavior of function calls in Scheme, and Clinger used it to specify in which sense an implementation should not run out of memory when processing a tail-recursive program (such as a program in CPS).

We first present a similar machine for the λ-calculus with left-to-right call-by-value evaluation and assignments. This machine is in the range of refocusing, transition compression, and closure unfolding, and so we next present the corresponding store-based calculus, λρ̂_{ptr}.

8.1 A simplified version of Clinger’s abstract machine

Our simplified version of Clinger’s abstract machine is an eval/apply machine with an environment and a store:

⟨x, s, C , σ⟩ ⇒_{ptr} ⟨C , σ(s(x)), σ⟩
⟨λx.t, s, C , σ⟩ ⇒_{ptr} ⟨C , (λx.t, s), σ⟩
⟨t_{0} t_{1}, s, C , σ⟩ ⇒_{ptr} ⟨t_{0}, s, C [[ ] (t_{1}, s)], σ⟩
⟨x := t, s, C , σ⟩ ⇒_{ptr} ⟨t, s, C [upd(s(x), [ ])], σ⟩
⟨[ ], v, σ⟩ ⇒_{ptr} (v, σ)
⟨C [[ ] (t, s)], v, σ⟩ ⇒_{ptr} ⟨t, s, C [v [ ]], σ⟩
⟨C [(λx.t, s) [ ]], v, σ⟩ ⇒_{ptr} ⟨t, (x, ℓ) · s, C , σ[ℓ ↦ v]⟩

if ℓ does not occur within s, C , v, σ

⟨C [upd(ℓ, [ ])], v, σ⟩ ⇒_{ptr} ⟨C , σ(ℓ), σ[ℓ ↦ v]⟩

Locations ℓ range over an unspecified set of locations. A store σ is a finite mapping from locations to value closures. Denotable values are locations.

Clinger’s machine also has a garbage-collection rule [19, Figure 5 and Section 3], but for simplicity we ignore it here.

8.2 The language of λρ̂_{ptr}

The abstract syntax of the language is as follows:

(terms)  t ::= x | λx.t | t t | x := t
(closures)  c ::= t[s] | c c
(values)  v ::= (λx.t)[s]
(substitutions) s ::= • | (x, ℓ) · s
(red. contexts) C ::= [ ] | C [[ ] c] | C [v [ ]] | C [upd(ℓ, [ ])]
(store)  σ ::= • | σ[ℓ ↦ v]
(store closures) c̃::= c[σ]
(store values) ṽ ::= v[σ]
(store contexts) C̃ ::= C [σ]

8.3 Notion of context-sensitive reduction

In the rules below, (Var) dereferences the store; (Beta) allocates a fresh location, and extends both the substitution and the store with it; (Prop) is context-insensitive and therefore essentially as in the λρ̂-calculus; and (Upd) updates the store.

(Var) ⟨x_{i}[(x_{1}, ℓ_{1}) ⋯ (x_{j}, ℓ_{j})], C [σ]⟩ →_{ptr} ⟨σ(ℓ_{i}), C [σ]⟩ if i ≤ j
(Beta)  ⟨((λx.t)[s]) v, C [σ]⟩ →_{ptr} ⟨t[(x, ℓ) · s], C [σ[ℓ ↦ v]]⟩

if ℓ does not occur within s, C , v, σ

(Prop)  ⟨(t_{0} t_{1})[s], C [σ]⟩ →_{ptr} ⟨(t_{0}[s]) (t_{1}[s]), C [σ]⟩
(Upd)  ⟨upd(ℓ, v), C [σ]⟩ →_{ptr} ⟨σ(ℓ), C [σ[ℓ ↦ v]]⟩

Refocusing, compressing the intermediate transitions, and unfolding the data type of closures mechanically yields the abstract machine of Section 8.1.

8.4 Formal correspondence

Proposition 12. For any term t in the λρ̂_{ptr}-calculus,

t[•][•] →_{ptr}^{∗} v[σ] if and only if ⟨t, •, [ ], •⟩ ⇒_{ptr}^{∗} (v, σ).

The λρ̂_{ptr}-calculus therefore directly corresponds to the simplified version of Clinger’s properly tail-recursive machine.

In Section 7, we showed storeless variants of two machines for stack inspection (the fg and the cm machines). The original versions of these machines use a store in the Clinger fashion [16], and we can exhibit their underlying calculi with an explicit representation of the store, as straightforward extensions of the storeless calculi. For conciseness, we do not include them here.

9 A lazy calculus of closures

The store-based account of proper tail-recursion from Section 8 suggests the following lazy calculus of closures, λρ̂_{l}.

9.1 The language of λρ̂_{l}

The abstract syntax of the language is as follows:

(terms)  t ::= i | λt | t t
(closures)  c ::= t[s] | c ℓ | upd(ℓ, c)
(values)  v ::= (λt)[s]
(substitutions)  s ::= • | ℓ · s
(reduction contexts) C ::= [ ] | C [[ ] ℓ] | C [upd(ℓ, [ ])]
(store)  σ ::= • | σ[ℓ ↦ v]
(store closures)  c̃::= c[σ]
(store values)  ṽ ::= v[σ]
(store contexts)  C̃ ::= C [σ]

9.2 Notion of context-sensitive reduction

The notion of reduction is specified by the five rules shown below.

(Var_{1}) ⟨i[ℓ_{1} ⋯ ℓ_{j}], C [σ]⟩ →_{l} ⟨v, C [σ]⟩  if σ(ℓ_{i}) = v
(Var_{2}) ⟨i[ℓ_{1} ⋯ ℓ_{j}], C [σ]⟩ →_{l} ⟨upd(ℓ_{i}, c), C [σ]⟩  if σ(ℓ_{i}) = c
(Beta) ⟨((λt)[s]) ℓ, C [σ]⟩ →_{l} ⟨t[ℓ · s], C [σ]⟩
(App) ⟨(t_{0} t_{1})[s], C [σ]⟩ →_{l} ⟨(t_{0}[s]) ℓ, C [σ[ℓ ↦ t_{1}[s]]]⟩ where ℓ does not occur in s, C , σ
(Upd) ⟨upd(ℓ, v), C [σ]⟩ →_{l} ⟨v, C [σ[ℓ ↦ v]]⟩

Variables denote locations, and have two reduction rules, depending on whether the store holds a value or not at that location. In the former case—handled by (Var_{1})—the result is this value, the current context, and the current store. In the latter case—handled by (Var_{2})—a special closure upd(ℓ, c) is created, indicating that c is a shared computation. When this computation completes and yields a value, the store at location ℓ should be updated with this value, which is achieved by (Upd). Since every argument to an application can potentially be shared, (App) conservatively allocates a new location in the store for such shared closures. (Beta) extends the substitution with this location.

9.3 An eval/apply abstract machine

Refocusing, compressing the intermediate transitions, and unfolding the data type of closures mechanically yields the following store-based machine:^{3}

⟨i, s, C , σ⟩ ⇒_{l} ⟨C , (λt′, s′), σ⟩  where s(i) = ℓ and σ(ℓ) = (λt′)[s′]
⟨i, s, C , σ⟩ ⇒_{l} ⟨t′, s′, C [upd(ℓ, [ ])], σ⟩  where s(i) = ℓ and σ(ℓ) = t′[s′]
⟨λt, s, C , σ⟩ ⇒_{l} ⟨C , (λt, s), σ⟩
⟨t_{0} t_{1}, s, C , σ⟩ ⇒_{l} ⟨t_{0}, s, C [[ ] ℓ], σ[ℓ ↦ (t_{1}, s)]⟩ where ℓ does not occur in s, C , σ

3When a shared closure is to be evaluated, the current context is extended with what is known as an ‘update marker’ in the Three Instruction Machine (denoted C [upd(ℓ, [ ])] here).

⟨[ ], v, σ⟩ ⇒_{l} (v, σ)
⟨C [[ ] ℓ], (λt, s), σ⟩ ⇒_{l} ⟨t, ℓ · s, C , σ⟩
⟨C [upd(ℓ, [ ])], v, σ⟩ ⇒_{l} ⟨C , v, σ[ℓ ↦ v]⟩

This lazy abstract machine coincides with the one derived by Ager et al. out of a call-by-need interpreter for the λ-calculus [3], thereby connecting the present syntactic correspondence between calculi and abstract machines with the functional correspondence between abstract machines and evaluators [2, 4, 7, 28].

9.4 Formal correspondence

Proposition 13. For any term t in the λρ̂_{l}-calculus,

t[•][•] →_{l}^{∗} v[σ] if and only if ⟨t, •, [ ], •⟩ ⇒_{l}^{∗} (v, σ).

The λρ̂_{l}-calculus therefore directly corresponds to call-by-need evaluation [85].

In λρ̂_{l}, sharing is made possible through a global heap where actual parameters are stored. On the other hand, a number of other calculi modeling call by need extend the set of terms with a local let-like construct, either by statically translating the source language into an intermediate language with explicit indications of sharing (as in Launchbury’s approach [63]), or by providing dynamic reduction rules to the same effect (as in Ariola et al.’s calculus [5]). A sequence of let constructs binding variables to shared computations is a local version of a global heap where shared computations are bound to locations; extra reductions are then needed to propagate all the let constructs to the top level.

Another specificity of λρ̂_{l} is that allocation occurs early, i.e., a new cell is allocated in the store every time an application is evaluated. Allocation, however, occurs late in Ariola et al.’s semantics, i.e., a new binding is created only when the operator of the application is known to be a λ-abstraction. Delaying allocation is useful in the presence of strict functions, which we do not consider here.

We can construct a local version of our calculus with either of the store propagated inside closures or of late allocation. From there, one can mechanically derive the corresponding abstract machines.

10 Conclusion

We have presented a series of calculi and abstract machines accounting for a variety of computational effects, making it possible to directly reason about a computation in the calculus and in the corresponding abstract machine (horizontally in the diagram below) and to directly account for actual and explicit substitutions both in the world of calculi and in the world of abstract machines (vertically in the diagram below, where σ maps a closure into the corresponding λ-term and an environment-machine configuration into a configuration in the corresponding machine with actual substitutions):

λ-calculus [figure]

syntactic correspondence [figure]

machine with actual substitutions

λρ̂-calculus [figure]

syntactic correspondence [figure] σ [figure]

environment-based machine σ [figure] The correspondence between each calculus and each abstract machine is simple and each can be mechanically built from the other. All of the calculi are new. Many of the abstract machines are known and have been independently designed and proved correct.

The work reported here leads us to drawing the following conclusions.

Curien’s calculus of closures: Once extended to account for one-step reduction, Curien’s calculus of closures directly corresponds to the notions of evaluation (i.e., weakhead normalization) accounted for by environment-based machines, even in the presence of computational effects (state and control).

Refocusing: Despite its pragmatic origin—fusing a plug function and a decomposition function in a reduction-based evaluation function to improve its efficiency [36], and in combination with compressing intermediate transitions and unfolding closures, refocusing proves consistently useful to construct reduction-free evaluation functions in the form of abstract machines, even in the presence of computational effects.

Defunctionalization: Despite its practical origin—representing a higher-order function as a data type and a dispatch function [72], defunctionalization proves consistently useful, witness the next item and also the fact that except for the abstract machines for λρ̂F and the cm machine, all the abstract machines in this article are in defunctionalized form.

Reduction contexts and evaluation contexts: There are three objective reasons— one extensional and two intensional—why contexts are useful as well as, in some sense, unavoidable:

• reduction contexts are in one-to-one correspondence with the compatibility rules of a calculus;

• reduction contexts are the data type of the defunctionalized continuation of a onestep reduction function (as used in a reduction-based (weak-head) normalization function); and

• evaluation contexts are the data type of the defunctionalized continuation of an evaluation function (as used in a reduction-free (weak-head) normalization function).

If nothing else, each of these three reasons has practical value as a guideline for writing the grammar of reduction / evaluation contexts (which can be tricky in practice). But more significantly [27], reduction contexts and evaluation contexts coincide, which means that as a data type, they mediate between one-step reduction and evaluation, given an appropriate dispatch function:

context

decompose′_{aux}

& plug

[figure]

[figure]

refocus_{aux}

[figure]

[figure]

state-transition functions

eval/apply abstract machine

one-step reduction function in CPS defunctionalization [figure]

evaluation function in CPS defunctionalization [figure] Indeed, as initiated by Reynolds [29,72], defunctionalizing a continuation-passing evaluator yields an abstract machine [2–4, 7], and as already pointed out above, a vast number of abstract machines are in defunctionalized form [9, 11, 28].

Together, the syntactic correspondence between calculi and abstract machines and the functional correspondence between abstract machines and evaluators therefore connect apparently distinct approaches to the same computational situations. We already illustrated this connection in Section 6 with delimited continuations; let us briefly illustrate it further with the simpler example of call/cc:

Call/cc was introduced in Scheme [17] as a Church encoding of Reynolds’s escape operator [72]. A typed version of it is available in Standard ML of New Jersey [52] and Griffin has identified its logical content [49]. It is endowed with a variety of specifications: a CPS transformation [33], a CPS interpreter [53,72], a denotational semantics [57], a computational monad [86], a big-step operational semantics [52], the CEK machine [43], calculi in the form of reduction semantics [42], and a number of implementation techniques [18, 25, 55]—not to mention its call-by-name version that allegedly accounts for the axiom of choice in the archival version of Krivine’s machine [60].

Question: How do we know that all the artifacts in this semantic jungle define the same call/cc?

The elements of answer we contribute here are that the syntactic correspondence links calculi and abstract machines, and the functional correspondence links abstract machines and evaluators. So by construction, all these specifications are inter-derivable and therefore they are consistent.

Normalization by evaluation: Finally, refocusing provides a guideline for constructing reduction-free normalization functions out of reduction-based ones [26]. The reductionfree normalization functions take the form of eval/apply abstract machines, which usually are in defunctionalized form, which paves the way to writing normalization functions as usually encountered in the area of normalization by evaluation [31]. We have illustrated the method here with weak reduction and weak-head normalization (i.e., evaluation), but it also works for strong reduction and normalization, thus linking one-step reduction, abstract machines for strong reduction, and normalization functions.

Acknowledgments

We are grateful to Julia Lawall and Kristian Støvring for commenting a preliminary version of this article.

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.

References

[1] Martín Abadi, Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques Lévy. Explicit substitutions. Journal of Functional Programming, 1(4):375–416, 1991.

[2] Mads Sig Ager, Dariusz Biernacki, Olivier Danvy, and Jan Midtgaard. A functional correspondence between evaluators and abstract machines. In Dale Miller, editor, Proceedings of the Fifth ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP’03), pages 8–19. ACM Press, August 2003.

[3] Mads Sig Ager, Olivier Danvy, and Jan Midtgaard. A functional correspondence between call-by-need evaluators and lazy abstract machines. Information Processing Letters, 90(5):223–232, 2004. Extended version available as the technical report BRICS RS-04-3.

[4] Mads Sig Ager, Olivier Danvy, and Jan Midtgaard. A functional correspondence between monadic evaluators and abstract machines for languages with computational effects. Theoretical Computer Science, 342(1):149–172, 2005. Extended version available as the technical report BRICS RS-04-28.

[5] Zena M. Ariola, Matthias Felleisen, John Maraist, Martin Odersky, and Philip Wadler. The call-by-need lambda calculus. In Peter Lee, editor, Proceedings of the Twenty-Second Annual ACM Symposium on Principles of Programming Languages, pages 233–246, San Francisco, California, January 1995. ACM Press.

[6] Zena M. Ariola and Hugo Herbelin. Minimal classical logic and control operators. In Jos C. M. Baeten, Jan Karel Lenstra, Joachim Parrow, and Gerhard J. Woeginger, editors, Automata, Languages and Programming, 30th International Colloquium (ICALP 2003), number 2719 in Lecture Notes in Computer Science, pages 871–885, Eindhoven, The Netherlands, July 2003. Springer.

[7] Małgorzata Biernacka, Dariusz Biernacki, and Olivier Danvy. An operational foundation for delimited continuations in the CPS hierarchy. Logical Methods in Computer Science, 1(2:5):1–39, November 2005. A preliminary version was presented at the Fourth ACM SIGPLAN Workshop on Continuations (CW’04).

[8] Małgorzata Biernacka and Olivier Danvy. A concrete framework for environment machines. Research Report BRICS RS-05-15, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, May 2005.

[9] Dariusz Biernacki and Olivier Danvy. From interpreter to logic engine by defunctionalization. In Maurice Bruynooghe, editor, Logic Based Program Synthesis and Transformation, 13th International Symposium, LOPSTR 2003, number 3018 in Lecture Notes in Computer Science, pages 143–159, Uppsala, Sweden, August 2003. Springer-Verlag.

[10] Dariusz Biernacki and Olivier Danvy. A simple proof of a folklore theorem about delimited control. Research Report BRICS RS-05-10, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, March 2005. Accepted for publication in the Journal of Functional Programming as a theoretical pearl.

[11] Dariusz Biernacki, Olivier Danvy, and Kevin Millikin. A dynamic continuationpassing style for dynamic delimited continuations. Research Report BRICS RS-05-16, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, May 2005.

[12] Dariusz Biernacki, Olivier Danvy, and Chung-chieh Shan. On the dynamic extent of delimited continuations. Information Processing Letters, 96(1):7–17, 2005. Extended version available as the technical report BRICS RS-05-13.

[13] Robert (Corky) Cartwright, editor. Proceedings of the 1988 ACM Conference on Lisp and Functional Programming, Snowbird, Utah, July 1988. ACM Press.

[14] Eugene Charniak, Christopher Riesbeck, and Drew McDermott. Artificial Intelligence Programming. Lawrence Earlbaum Associates, 1980.

[15] Alonzo Church. The Calculi of Lambda-Conversion. Princeton University Press, 1941.

[16] John Clements and Matthias Felleisen. A tail-recursive semantics for stack inspection. ACM Transactions on Programming Languages and Systems, 26(6):1029–1052, 2004.

[17] William Clinger, Daniel P. Friedman, and Mitchell Wand. A scheme for a higher-level semantic algebra. In John Reynolds and Maurice Nivat, editors, Algebraic Methods in Semantics, pages 237–250. Cambridge University Press, 1985.

[18] William Clinger, Anne H. Hartheimer, and Eric M. Ost. Implementation strategies for first-class continuations. Higher-Order and Symbolic Computation, 12(1):7–45, 1999.

[19] William D. Clinger. Proper tail recursion and space efficiency. In Keith D. Cooper, editor, Proceedings of the ACM SIGPLAN’98 Conference on Programming Languages Design and Implementation, pages 174–185, Montréal, Canada, June 1998. ACM Press.

[20] Pierre Crégut. An abstract machine for lambda-terms normalization. In Wand [88], pages 333–340.

[21] Pierre Crégut. Strongly reducing variants of the Krivine abstract machine. In Danvy [30]. To appear. Journal version of [20].

[22] Pierre-Louis Curien. Categorical Combinators, Sequential Algorithms and Functional Programming, volume 1 of Research Notes in Theoretical Computer Science. Pitman, 1986.

[23] Pierre-Louis Curien. An abstract framework for environment machines. Theoretical Computer Science, 82:389–402, 1991.

[24] Pierre-Louis Curien, Thérèse Hardin, and Jean-Jacques Lévy. Confluence properties of weak and strong calculi of explicit substitutions. Journal of the ACM, 43(2):362– 397, 1996.

[25] Olivier Danvy. Formalizing implementation strategies for first-class continuations. In Gert Smolka, editor, Proceedings of the Ninth European Symposium on Programming, number 1782 in Lecture Notes in Computer Science, pages 88–103, Berlin, Germany, March 2000. Springer-Verlag.

[26] Olivier Danvy. From reduction-based to reduction-free normalization. In Sergio Antoy and Yoshihito Toyama, editors, Proceedings of the Fourth International Workshop on Reduction Strategies in Rewriting and Programming (WRS’04), number 124 in Electronic Notes in Theoretical Computer Science, pages 79–100, Aachen, Germany, May 2004. Elsevier Science. Invited talk.

[27] Olivier Danvy. On evaluation contexts, continuations, and the rest of the computation. In Hayo Thielecke, editor, Proceedings of the Fourth ACM SIGPLAN Workshop on Continuations (CW’04), Technical report CSR-04-1, Department of Computer Science, Queen Mary’s College, pages 13–23, Venice, Italy, January 2004. Invited talk.

[28] Olivier Danvy. A rational deconstruction of Landin’s SECD machine. In Clemens Grelck, Frank Huch, Greg J. Michaelson, and Phil Trinder, editors, Implementation and Application of Functional Languages, 16th International Workshop, IFL’04, number 3474 in Lecture Notes in Computer Science, pages 52–71, Lübeck, Germany, September 2004. Springer-Verlag. Recipient of the 2004 Peter Landin prize. Extended version available as the technical report BRICS RS-03-33.

[29] Olivier Danvy. Defunctionalized interpreters for higher-order programming languages. In Preliminary proceedings of the 21st Conference on Mathematical Foundations of Programming Semantics, Birmingham, UK, May 2005. John Reynolds session.

[30] Olivier Danvy, editor. Special Issue on the Krivine Abstract Machine, Higher-Order and Symbolic Computation. Springer, 2006. In preparation.

[31] Olivier Danvy and Peter Dybjer, editors. Proceedings of the 1998 APPSEM Workshop on Normalization by Evaluation (NBE 1998), BRICS Note Series NS-98-8, Gothenburg, Sweden, May 1998. BRICS, Department of Computer Science, University of Aarhus.

[32] Olivier Danvy and Andrzej Filinski. Abstracting control. In Wand [88], pages 151–160.

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

[34] Olivier Danvy and Karoline Malmkjær. Intensions and extensions in a reflective tower. In Cartwright [13], pages 327–341.

[35] Olivier Danvy and Lasse R. Nielsen. Defunctionalization at work. In Harald Søndergaard, editor, Proceedings of the Third International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP’01), pages 162–174, Firenze, Italy, September 2001. ACM Press. Extended version available as the technical report BRICS RS-01-23.

[36] Olivier Danvy and Lasse R. Nielsen. Refocusing in reduction semantics. Research Report BRICS RS-04-26, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, November 2004. A preliminary version appears in the informal proceedings of the Second International Workshop on Rule-Based Programming (RULE 2001), Electronic Notes in Theoretical Computer Science, Vol. 59.4.

[37] Olivier Danvy and Zhe Yang. An operational investigation of the CPS hierarchy. In S. Doaitse Swierstra, editor, Proceedings of the Eighth European Symposium on Programming, number 1576 in Lecture Notes in Computer Science, pages 224–242, Amsterdam, The Netherlands, March 1999. Springer-Verlag.

[38] Philippe de Groote. An environment machine for the lambda-mu-calculus. Mathematical Structures in Computer Science, 8:637–669, 1998.

[39] R. Kent Dybvig, Simon Peyton-Jones, and Amr Sabry. A monadic framework for subcontinuations. Technical Report 615, Computer Science Department, Indiana University, Bloomington, Indiana, June 2005.

[40] Matthias Felleisen. The Calculi of λ-v-CS Conversion: A Syntactic Theory of Control and State in Imperative Higher-Order Programming Languages. PhD thesis, Computer Science Department, Indiana University, Bloomington, Indiana, August 1987.

[41] Matthias Felleisen. The theory and practice of first-class prompts. In Jeanne Ferrante and Peter Mager, editors, Proceedings of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, pages 180–190, San Diego, California, January 1988. ACM Press.

[42] Matthias Felleisen and Matthew Flatt. Programming languages and lambda cal-

culi. Unpublished lecture notes. http://www.ccs.neu.edu/home/matthias/3810-w02/
readings.html, 1989-2003.

[43] Matthias Felleisen and Daniel P. Friedman. Control operators, the SECD machine, and the λ-calculus. In Martin Wirsing, editor, Formal Description of Programming Concepts III, pages 193–217. Elsevier Science Publishers B.V. (North-Holland), Amsterdam, 1986.

[44] Matthias Felleisen, Daniel P. Friedman, Bruce Duba, and John Merrill. Beyond continuations. Technical Report 216, Computer Science Department, Indiana University, Bloomington, Indiana, February 1987.

[45] Matthias Felleisen, Mitchell Wand, Daniel P. Friedman, and Bruce F. Duba. Abstract continuations: A mathematical semantics for handling full functional jumps. In Cartwright [13], pages 52–62.

[46] Andrzej Filinski. Representing layered monads. In Alex Aiken, editor, Proceedings of the Twenty-Sixth Annual ACM Symposium on Principles of Programming Languages, pages 175–188, San Antonio, Texas, January 1999. ACM Press.

[47] Cédric Fournet and Andrew D. Gordon. Stack inspection: Theory and variants. ACM Transactions on Programming Languages and Systems, 25(3):360–399, May 2003.

[48] Steven E. Ganz, Daniel P. Friedman, and Mitchell Wand. Trampolined style. In Peter Lee, editor, Proceedings of the 1999 ACM SIGPLAN International Conference on Functional Programming, pages 18–27, Paris, France, September 1999. ACM Press.

[49] Timothy G. Griffin. A formulae-as-types notion of control. In Paul Hudak, editor, Proceedings of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, pages 47–58, San Francisco, California, January 1990. ACM Press.

[50] Carl Gunter, Didier Rémy, and Jon G. Riecke. A generalization of exceptions and control in ML-like languages. In Simon Peyton Jones, editor, Proceedings of the Seventh ACM Conference on Functional Programming and Computer Architecture, pages 12–23, La Jolla, California, June 1995. ACM Press.

[51] Thérèse Hardin, Luc Maranget, and Bruno Pagano. Functional runtime systems within the lambda-sigma calculus. Journal of Functional Programming, 8(2):131–172, 1998.

[52] Robert Harper, Bruce F. Duba, and David MacQueen. Typing first-class continuations in ML. Journal of Functional Programming, 3(4):465–484, October 1993.

[53] Christopher T. Haynes, Daniel P. Friedman, and Mitchell Wand. Continuations and coroutines. In Guy L. Steele Jr., editor, Conference Record of the 1984 ACM Symposium on Lisp and Functional Programming, pages 293–298, Austin, Texas, August 1984. ACM Press.

[54] Carl Hewitt. Control structure as patterns of passing messages. In Patrick Henry Winston and Richard Henry Brown, editors, Artificial Intelligence: An MIT Perspective, volume 2, pages 434–465. The MIT Press, 1979.

[55] Robert Hieb, R. Kent Dybvig, and Carl Bruggeman. Representing control in the presence of first-class continuations. In Bernard Lang, editor, Proceedings of the ACM SIGPLAN’90 Conference on Programming Languages Design and Implementation, SIGPLAN Notices, Vol. 25, No 6, pages 66–77, White Plains, New York, June 1990. ACM Press.

[56] Yukiyoshi Kameyama. Axioms for delimited continuations in the CPS hierarchy. In Jerzy Marcinkowski and Andrzej Tarlecki, editors, Computer Science Logic, 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Proceedings, volume 3210 of Lecture Notes in Computer Science, pages 442–457, Karpacz, Poland, September 2004. Springer.

[57] Richard Kelsey, William Clinger, and Jonathan Rees, editors. Revised^{5} report on the algorithmic language Scheme. Higher-Order and Symbolic Computation, 11(1):7–105, 1998.

[58] Oleg Kiselyov. How to remove a dynamic prompt: Static and dynamic delimited continuation operators are equally expressible. Technical Report 611, Computer Science Department, Indiana University, Bloomington, Indiana, March 2005.

[59] Jean-Louis Krivine. Un interprète du λ-calcul. Brouillon. Available online at http:

//www.pps.jussieu.fr/~krivine/, 1985.

[60] Jean-Louis Krivine. A call-by-name lambda-calculus machine. In Danvy [30]. To

appear. Available online at http://www.pps.jussieu.fr/~krivine/.

[61] Peter J. Landin. The mechanical evaluation of expressions. The Computer Journal, 6(4):308–320, 1964.

[62] Peter J. Landin. A generalization of jumps and labels. Technical report, UNIVAC Systems Programming Research, 1965. Reprinted in Higher-Order and Symbolic Computation 11(2):125–143, 1998, with a foreword [84].

[63] John Launchbury. A natural semantics for lazy evaluation. In Susan L. Graham, editor, Proceedings of the Twentieth Annual ACM Symposium on Principles of Programming Languages, pages 144–154, Charleston, South Carolina, January 1993. ACM Press.

[64] Xavier Leroy. The Zinc experiment: an economical implementation of the ML language. Rapport Technique 117, INRIA Rocquencourt, Le Chesnay, France, February 1990.

[65] Pierre Lescanne. From λσ to λv a journey through calculi of explicit substitutions. In Hans-J. Boehm, editor, Proceedings of the Twenty-First Annual ACM Symposium on Principles of Programming Languages, pages 60–69, Portland, Oregon, January 1994. ACM Press.

[66] Simon Marlow and Simon L. Peyton Jones. Making a fast curry: push/enter vs. eval/apply for higher-order languages. In Kathleen Fisher, editor, Proceedings of the 2004 ACM SIGPLAN International Conference on Functional Programming, SIGPLAN Notices, Vol. 39, No. 9, pages 4–15, Snowbird, Utah, September 2004. ACM Press.

[67] John McCarthy. Recursive functions of symbolic expressions and their computation by machine, part I. Communications of the ACM, 3(4):184–195, 1960.

[68] Peter D. Mosses. A foreword to ‘Fundamental concepts in programming languages’. Higher-Order and Symbolic Computation, 13(1/2):7–9, 2000.

[69] Michel Parigot. λμ-calculus: an algorithmic interpretation of classical natural deduction. In Andrei Voronkov, editor, Proceedings of the International Conference on Logic Programming and Automated Reasoning, number 624 in Lecture Notes in Artificial Intelligence, pages 190–201, St. Petersburg, Russia, July 1992. Springer-Verlag.

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

[71] François Pottier, Christian Skalka, and Scott Smith. A systematic approach to static access control. ACM Transactions on Programming Languages and Systems, 27(2), 2005.

[72] John C. Reynolds. Definitional interpreters for higher-order programming languages. In Proceedings of 25th ACM National Conference, pages 717–740, Boston, Massachusetts, 1972. Reprinted in Higher-Order and Symbolic Computation 11(4):363– 397, 1998, with a foreword [74].

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

[74] John C. Reynolds. Definitional interpreters revisited. Higher-Order and Symbolic Computation, 11(4):355–361, 1998.

[75] Kristoffer H. Rose. Explicit substitution – tutorial & survey. BRICS Lecture Series LS-96-3, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, September 1996.

[76] Erik Sandewall. An early use of continuations and partial evaluation for compiling rules written in FOPC. Higher-Order and Symbolic Computation, 12(1):105–113, 1999.

[77] Chung-chieh Shan. Shift to control. In Olin Shivers and Oscar Waddell, editors, Proceedings of the 2004 ACM SIGPLAN Workshop on Scheme and Functional Programming, Technical report TR600, Computer Science Department, Indiana University, Snowbird, Utah, September 2004.

[78] Dorai Sitaram and Matthias Felleisen. Control delimiters and their hierarchies. Lisp and Symbolic Computation, 3(1):67–99, January 1990.

[79] Brian C. Smith. Reflection and semantics in Lisp. In Ken Kennedy, editor, Proceedings of the Eleventh Annual ACM Symposium on Principles of Programming Languages, pages 23–35, Salt Lake City, Utah, January 1984. ACM Press.

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

[81] Christopher Strachey. Fundamental concepts in programming languages. International Summer School in Computer Programming, Copenhagen, Denmark, August 1967. Reprinted in Higher-Order and Symbolic Computation 13(1/2):11–49, 2000, with a foreword [68].

[82] Christopher Strachey and Christopher P. Wadsworth. Continuations: A mathematical semantics for handling full jumps. Technical Monograph PRG-11, Oxford University Computing Laboratory, Programming Research Group, Oxford, England, 1974. Reprinted in Higher-Order and Symbolic Computation 13(1/2):135–152, 2000, with a foreword [87].

[83] Gerald J. Sussman and Guy L. Steele Jr. SCHEME: An interpreter for extended lambda calculus. AI Memo 349, Artificial Intelligence Laboratory, Massachusetts Institute of Technology, Cambridge, Massachusetts, December 1975. Reprinted in Higher-Order and Symbolic Computation 11(4):405–439, 1998, with a foreword.

[84] Hayo Thielecke. An introduction to Landin’s “A generalization of jumps and labels”. Higher-Order and Symbolic Computation, 11(2):117–124, 1998.

[85] Jean Vuillemin. Correct and optimal implementations of recursion in a simple programming language. Journal of Computer and System Sciences, 9(3):332–354, 1974.

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

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

[88] Mitchell Wand, editor. Proceedings of the 1990 ACM Conference on Lisp and Functional Programming, Nice, France, June 1990. ACM Press.

[89] Mitchell Wand and Daniel P. Friedman. The mystery of the tower revealed: A nonreflective description of the reflective tower. Lisp and Symbolic Computation, 1(1):11– 38, May 1988.

Recent BRICS Report Series Publications

RS-05-38 Ma�gorzata Biernacka and Olivier Danvy. A Syntactic Correspondence between Context-Sensitive Calculi and Abstract Machines. December 2005. iii+39 pp. Revised version of BRICS RS-05-22.

RS-05-37 Gerth Stølting Brodal, Kanela Kaligosi, Irit Katriel, and Martin Kutz. Faster Algorithms for Computing Longest Common Increasing Subsequences. December 2005. 16 pp.

RS-05-36 Dariusz Biernacki, Olivier Danvy, and Chung-chieh Shan. On the Static and Dynamic Extents of Delimited Continuations. December 2005. ii+33 pp. To appear in the journal Science of Computer Programming. Supersedes BRICS RS-05-13.

RS-05-35 Kristian Støvring. Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative. November 2005. 19 pp. To appear in Logical Methods in Computer Science.

RS-05-34 Henning Korsholm Rohde. Formal Aspects of Polyvariant Specialization. November 2005. 27 pp.

RS-05-33 Luca Aceto, Willem Jan Fokkink, Anna Ingólfsdóttir, and Sumit Nain. Bisimilarity is not Finitely Based over BPA with Interrupt. October 2005. 33 pp. This paper supersedes BRICS Report RS-04-24. An extended abstract of this paper appeared in Algebra and Coalgebra in Computer Science, 1st Conference, CALCO 2005, Swansea, Wales, 3–6 September 2005, Lecture Notes in Computer Science 3629, pp. 54–68, Springer-Verlag, 2005.

RS-05-32 Anders Møller, Mads Østerby Olesen, and Michael I. Schwartzbach. Static Validation of XSL Transformations. October 2005. 50 pp.

RS-05-31 Christian Kirkegaard and Anders Møller. Type Checking with XML Schema in Xact. September 2005. 20 pp.

RS-05-30 Karl Krukow. An Operational Semantics for Trust Policies. September 2005. 38 pp.

RS-05-29 Olivier Danvy and Henning Korsholm Rohde. On Obtaining the Boyer-Moore String-Matching Algorithm by Partial Evaluation. September 2005. ii+9 pp. To appear in Information Processing Letters. This version supersedes BRICS RS-05-14.