Abstract The equivalence of folding left and right over Peano numbers and lists makes it possible to minimalistically inter-derive (1) structurally recursive functions in direct style, (2) structurally tail-recursive functions that use an accumulator, and (3) structurally tail-recursive functions in delimited continuation-passing style, using Ohori and Sasano’s lightweight fusion by fixed-point promotion. When the fold-left and the fold-right functions account for primitive iteration for Peano numbers, this equivalence is unconditional. When they account for primitive recursion for Peano numbers, this equivalence is modulo left permutativity of their induction-step parameter – a property which is more general than associativity and commutativity. And when they account for primitive iteration or for primitive recursion over lists, this equivalence is modulo left permutativity of their induction-step parameter if these two fold functions have the same type. Since the 1980s, however, the two fold functions for lists do not have the same type: the arguments for their induction-step parameter are swapped, a re-ordering that complicated Bird and Wadler’s duality theorems and whose history is reviewed in an appendix. Without this re-ordering, Bird and Wadler’s second duality theorem more visibly accounts for “re-bracketing,” which is a key step to make recursive programs tail recursive in the general area of program development, from Cooper in the 1960s and onwards.

In the tortoise-and-hare algorithm, when the fast pointer reaches the end of a finite list, the slow pointer points to the middle of this list. In the early 2000’s, this property was found to make it possible to program a palindrome detector for immutable lists that operates in one recursive traversal of the given list and performs the smallest possible number of comparisons, using the “There And Back Again” (TABA) recursion pattern. In this article, this palindrome detector is reconstructed in OCaml, formalized with the Coq Proof Assistant, and proved to be correct. More broadly, this article presents a compositional account of the tortoise-and-hare algorithm for finite lists. Concretely, compositionality means that programs that use a fast and a slow pointer can be expressed with an ordinary fold function for lists and reasoned about using ordinary structural induction on the given list. This article also contains a dozen new applications of the TABA recursion pattern and of its tail-recursive variant, “There and Forth Again”.

"There and Back Again" (TABA) is a programming pattern where the recursive calls traverse one data structure and the subsequent returns traverse another. This article presents new TABA examples, refines existing ones, and formalizes both their control flow and their data flow using the Coq Proof Assistant. Each formalization mechanizes a pen-and-paper proof, thus making it easier to "get" TABA. In addition, this article identifies and illustrates a tail-recursive variant of TABA, There and Forth Again (TAFA) that does not come back but goes forth instead with more tail calls. Comment: 69 pages (final version with complete acknowledgments)

Abstract Fold–unfold lemmas complement the rewrite tactic in the Coq Proof Assistant to reason about recursive functions, be they defined locally or globally. Each of the structural cases gives rise to a fold–unfold lemma that equates a call to this function in that case with the corresponding case branch. As such, they are “boilerplate” and can be generated mechanically, though stating them by hand is a learning experience for a beginner, to say nothing about explaining them. Their proof is generic. Their use is precise (e.g., in terms with multiple calls) and they scale seamlessly (e.g., to continuation-passing style and to various patterns of recursion), be the reasoning equational or relational. In the author’s experience, they prove effective in the classroom, considering the clarity of discourse in the subsequent term reports and oral exams, and beyond the classroom, considering their subsequent use when continuing to work with the Coq Proof Assistant. Fold–unfold lemmas also provide a measure of understanding as well as of control about what is cut short when one uses a shortcut, i.e., an automated simplification tactic. Since Version 8.0, the functional-induction plugin provides them for functions that are defined globally, i.e., recursive equations, and so does the Equations plugin now, both for global and for local declarations, a precious help for advanced users.

For example, consider the standard powerset function that maps the representation of a set as the list of its elements (in any order and without repetition) to the representation of its powerset:Definition powerset (V : Type) (vs : list V)

We put a preexisting definitional abstract machine for dynamic delimited continuations in defunctionalized form, and we present the consequences of this adjustment. We first prove the correctness of the adjusted abstract machine. Because it is in defunctionalized form, we can refunctionalize it into a higher-order evaluation function. This evaluation function, which is compositional, is in continuation+state-passing style and threads a trail of delimited continuations and a meta-continuation. Since this style accounts for dynamic delimited continuations, we refer to it as “dynamic continuation-passing style” and we present the corresponding dynamic CPS transformation. We show that the notion of computation induced by dynamic CPS takes the form of a continuation monad with a recursive answer type. This continuation monad suggests a new simulation of dynamic delimited continuations in terms of static ones. Finally, we present new applications of dynamic delimited continuations, including a meta-circular evaluator. The significance of the present work is that the computational artifacts surrounding dynamic CPS are not independent designs: they are mechanical consequences of having put the definitional abstract machine in defunctionalized form.

We present the first operational account of call by need that connects syntactic theory and implementation practice. Syntactic theory: the storeless operational semantics using syntax rewriting to account for demand-driven computation and for caching intermediate results. Implementational practice: the store-based operational technique using memo-thunks to implement demand-driven computation and to cache intermediate results for subsequent sharing. The implementational practice was initiated by Landin and Wadsworth and is prevalent today to implement lazy programming languages such as Haskell. The syntactic theory was initiated by Ariola, Felleisen, Maraist, Odersky and Wadler and is prevalent today to reason equationally about lazy programs, on par with Barendregt et al.'s term graphs. Nobody knows, however, how the theory of call by need compares to the practice of call by need: all that is known is that the theory of call by need agrees with the theory of call by name, and that the practice of call by need optimizes the practice of call by name.

We present a purely syntactic theory of graph reduction for the canonical combinators S, K, and I, where graph vertices are represented with evaluation contexts and let expressions. We express this first syntactic theory as a storeless reduction semantics of combinatory terms. We then factor out the introduction of let expressions to denote as many graph vertices as possible upfront instead of on demand . The factored terms can be interpreted as term graphs in the sense of Barendregt et al. We express this second syntactic theory, which we prove equivalent to the first, as a storeless reduction semantics of combinatory term graphs. We then recast let bindings as bindings in a global store, thus shifting, in Strachey's words, from denotable entities to storable entities. The store-based terms can still be interpreted as term graphs. We express this third syntactic theory, which we prove equivalent to the second, as a store-based reduction semantics of combinatory term graphs. We then refocus this store-based reduction semantics into a store-based abstract machine. The architecture of this store-based abstract machine coincides with that of Turner's original reduction machine. The three syntactic theories presented here therefore properly account for combinatory graph reduction As We Know It. These three syntactic theories scale to handling the Y combinator. This article therefore illustrates the scientific consensus of theoreticians and implementors about graph reduction: it is the same combinatory elephant.

This tech talk describes how to write and how to inter-derive formal semantics for sequential programming languages. The progress reported here is (1) concrete guidelines to write each formal semantics to alleviate their proof obligations, and (2) simple calculational tools to obtain a formal semantics from another.

To celebrate the 20th anniversary of PEPM, we are inviting you to a walk in the semantic park and to inter-derive reduction-based and reduction-free negational normalization functions.

This document illustrates how functional implementations of formal semantics (structural operational semantics, reduction semantics, small-step and big-step abstract machines, natural semantics, and denotational semantics) can be transformed into each other. These transformations were foreshadowed by Reynolds in "Definitional Interpreters for Higher-Order Programming Languages" for functional implementations of denotational semantics, natural semantics, and big-step abstract machines using closure conversion, CPS transformation, and defunctionalization. Over the last few years, the author and his students have further observed that functional implementations of small-step and of big-step abstract machines are related using fusion by fixed-point promotion and that functional implementations of reduction semantics and of small-step abstract machines are related using refocusing and transition compression. It furthermore appears that functional implementations of structural operational semantics and of reduction semantics are related as well, also using CPS transformation and defunctionalization. This further relation provides an element of answer to Felleisen's conjecture that any structural operational semantics can be expressed as a reduction semantics: for deterministic languages, a reduction semantics is a structural operational semantics in continuation style, where the reduction context is a defunctionalized continuation. As the defunctionalized counterpart of the continuation of a one-step reduction function, a reduction context represents the rest of the reduction, just as an evaluation context represents the rest of the evaluation since it is the defunctionalized counterpart of the continuation of an evaluation function.

Landin's SECD machine was the first abstract machine for applicative expressions, i.e., functional programs. Landin's J operator was the first control operator for functional languages, and was specified by an extension of the SECD machine. We present a family of evaluation functions corresponding to this extension of the SECD machine, using a series of elementary transformations (transformation into continu-ation-passing style (CPS) and defunctionalization, chiefly) and their left inverses (transformation into direct style and refunctionalization). To this end, we modernize the SECD machine into a bisimilar one that operates in lockstep with the original one but that (1) does not use a data stack and (2) uses the caller-save rather than the callee-save convention for environments. We also identify that the dump component of the SECD machine is managed in a callee-save way. The caller-save counterpart of the modernized SECD machine precisely corresponds to Thielecke's double-barrelled continuations and to Felleisen's encoding of J in terms of call/cc. We then variously characterize the J operator in terms of CPS and in terms of delimited-control operators in the CPS hierarchy. As a byproduct, we also present several reduction semantics for applicative expressions with the J operator, based on Curien's original calculus of explicit substitutions. These reduction semantics mechanically correspond to the modernized versions of the SECD machine and to the best of our knowledge, they provide the first syntactic theories of applicative expressions with the J operator.

Over forty years ago, David Barron and Christopher Strachey published a startlingly elegant program for the Cartesian product of a list of lists, expressing it with a three nested occurrences of the function we now call foldr. This program is remarkable for its time because of its masterful display of higher-order functions and lexical scope, and we put it forward as possibly the first ever functional pearl. We first characterize it as the result of a sequence of program transformations, and then apply similar transformations to a program for the classical power set example. We also show that using a higher-order representation of lists allows a definition of the Cartesian product function where foldr is nested only twice.

Abstract We bridge two distinct approaches to one-pass CPS transformations, i.e, CPS transformations that reduce administrative redexes at transformation time instead of in a post-processing phase. One approach is compositional and higher-order, and is independently due to Appel, Danvy and Filinski, and Wand, building on Plotkin's seminal work. The other is non-compositional and based on a reduction semantics for the lambda-calculus, and is due to Sabry and Felleisen. To relate the two approaches, we use three tools: Reynolds's defunctionalization and its left inverse, refunctionalization; a special case of fold–unfold fusion due to Ohori and Sasano, fixed-point promotion; and an implementation technique for reduction semantics due to Danvy and Nielsen, refocusing. This work is directly applicable to transforming programs into monadic normal form.

We materialize the common understanding that calculi with explicit substitutions provide an intermediate step between an abstract specification of substitution in the lambda-calculus and its concrete implementations. To this end, we go back to Curien's original calculus of closures (an early calculus with explicit substitutions), we extend it minimally so that it can also express one-step reduction strategies, and we methodically derive a series of environment machines from the specification of two one-step reduction strategies for the lambda-calculus: normal order and applicative order. The derivation extends Danvy and Nielsen's refocusing-based construction of abstract machines with two new steps: one for coalescing two successive transitions into one, and the other for unfolding a closure into a term and an environment in the resulting abstract machine. The resulting environment machines include both the Krivine machine and the original version of Krivine's machine, Felleisen et al.'s CEK machine, and Leroy's Zinc abstract machine.

We formalize and prove the folklore theorem that the static delimited-control operators shift and reset can be simulated in terms of the dynamic delimited-control operators control and prompt. The proof is based on small-step operational semantics.

We show how to obtain all of Knuth, Morris, and Pratt's linear-time string matcher by specializing a quadratic-time string matcher with respect to a pattern string. Although it has been known for fifteen years how to obtain this linear matcher by partial evaluation of a quadratic one, how to obtain it in linear time has remained an open problem.Obtaining a linear matcher by the partial evaluation of a quadratic one is achieved by performing its backtracking at specialization time and memoizing its results. We show (1) how to rewrite the source matcher such that its static intermediate computations can be shared at specialization time and (2) how to extend the memoization capabilities of a partial evaluator to static functions. Such an extended partial evaluator, if its memoization is implemented efficiently, specializes the rewritten source matcher in linear time. Finally, we show that the method also applies to a variant of Boyer and Moore's string matcher.

We present an abstract machine and a reduction semantics for the lambda-calculus extended with control operators that give access to delimited continuations in the CPS hierarchy. The abstract machine is derived from an evaluator in continuation-passing style (CPS); the reduction semantics (i.e., a small-step operational semantics with an explicit representation of evaluation contexts) is constructed from the abstract machine; and the control operators are the shift and reset family. We also present new applications of delimited continuations in the CPS hierarchy: finding list prefixes and normalization by evaluation for a hierarchical language of units and products.

We show how to obtain all of Knuth, Morris, and Pratt's linear-time string matcher by partial evaluation of a quadratic-time string matcher with respect to a pattern string. Although it has been known for 15 years how to obtain this linear matcher by partial evaluation of a quadratic one, how to obtain it in linear time has remained an open problem.Obtaining a linear matcher by partial evaluation of a quadratic one is achieved by performing its backtracking at specialization time and memoizing its results. We show (1) how to rewrite the source matcher such that its static intermediate computations can be shared at specialization time and (2) how to extend the memoization capabilities of a partial evaluator to static functions. Such an extended partial evaluator, if its memoization is implemented efficiently, specializes the rewritten source matcher in linear time.

We bridge the gap between functional evaluators and abstract machines for the λ-calculus, using closure conversion, transformation into continuation-passing style, and defunctionalization.We illustrate this approach by deriving Krivine's abstract machine from an ordinary call-by-name evaluator and by deriving an ordinary call-by-value evaluator from Felleisen et al.'s CEK machine. The first derivation is strikingly simpler than what can be found in the literature. The second one is new. Together, they show that Krivine's abstract machine and the CEK machine correspond to the call-by-name and call-by-value facets of an ordinary evaluator for the λ-calculus.We then reveal the denotational content of Hannan and Miller's CLS machine and of Landin's SECD machine. We formally compare the corresponding evaluators and we illustrate some degrees of freedom in the design spaces of evaluators and of abstract machines for the λ-calculus with computational effects.Finally, we consider the Categorical Abstract Machine and the extent to which it is more of a virtual machine than an abstract machine.

We show that a non-duplicating transformation into Continuation-Passing Style (CPS) has no effect on control-flow analysis, a positive effect on binding-time analysis for traditional partial evaluation, and no effect on binding-time analysis for continuation-based partial evaluation: a monovariant control-flow analysis yields equivalent results on a direct-style program and on its CPS counterpart, a monovariant binding-time analysis yields less precise results on a direct-style program than on its CPS counterpart, and an enhanced monovariant binding-time analysis yields equivalent results on a direct-style program and on its CPS counterpart. Our proof technique amounts to constructing the CPS counterpart of flow information and of binding times. Our results formalize and confirm a folklore theorem about traditional binding-time analysis, namely that CPS has a positive effect on binding times. What may be more surprising is that the benefit does not arise from a standard refinement of program analysis, as, for instance, duplicating continuations. The present study is symptomatic of an unsettling property of program analyses: their quality is unpredictably vulnerable to syntactic accidents in source programs, i.e., to the way these programs are written. More reliable program analyses require a better understanding of the effect of syntactic change.

We characterize the impact of a linear $\beta$ -reduction on the result of a control-flow analysis. (By ‘a linear $\beta$ -reduction’ we mean the $\beta$ -reduction of a linear $\lambda$ -abstraction, i.e., of a $\lambda$ -abstraction whose parameter occurs exactly once in its body.) As a corollary, we consider the administrative reductions of a Plotkin-style transformation into Continuation-Passing Style (CPS), and how they affect the result of a constraint-based control-flow analysis and, in particular, the least element in the space of solutions. We show that administrative reductions preserve the least solution. Preservation of least solutions solves a problem that was left open in Palsberg and Wand's article ‘CPS Transformation of Flow Information.’ Together, Palsberg and Wand's article and the present article show how to map in linear time the least solution of the flow constraints of a program into the least solution of the flow constraints of the CPS counterpart of this program, after administrative reductions. Furthermore, we show how to CPS transform control-flow information in one pass.

We present a programming pattern where a recursive function traverses a data structure---typically a list---at return time. The idea is that the recursive calls get us there (typically to a base case) and the returns get us back again while traversing the data structure. We name this programming pattern of traversing a data structure at return time "There And Back Again" (TABA).The TABA pattern directly applies to computing a symbolic convolution. It also synergizes well with other programming patterns, e.g., dynamic programming and traversing a list at double speed. We illustrate TABA and dynamic programming with Catalan numbers. We illustrate TABA and traversing a list at double speed with palindromes and we obtain a novel solution to this traditional exercise.A TABA-based function written in direct style makes full use of an Algol-like control stack and needs no heap allocation. Conversely, in a TABA-based function written in continuation-passing style, the continuation acts as a list iterator. In general, the TABA pattern saves one from constructing intermediate lists in reverse order.

Reynolds's defunctionalization technique is a whole-program transformation from higher-order to first-order functional programs. We study practical applications of this transformation and uncover new connections between seemingly unrelated higher-order and first-order specifications and between their correctness proofs. Defunctionalization therefore appearsboth as a springboard for rev ealing new connections and as a bridge for transferring existing results between the first-order world and the higher-order world.

In higher-order abstract syntax, the variables and bindings of an object language are represented by variables and bindings of a meta-language. Let us consider the simply typed λ-calculus as object language and Haskell as meta-language. For concreteness, we also throw in integers and addition, but only in this section.

We show that a non-duplicating CPS transformation has no effect on control-flow analysis and that it has a positive effect on binding-time analysis: a monovariant control-flow analysis yields equivalent results on a direct-style program and on its CPS counterpart, and a monovariant binding-time analysis yields more precise results on a CPS program than on its direct-style counterpart. Our proof technique amounts to constructing the continuation-passing style (CPS) counterpart of flow information and of binding times.Our results confirm a folklore theorem about binding-time analysis, namely that CPS has a positive effect on binding times. What may be more surprising is that this benefit holds even if contexts or continuations are not duplicated.The present study is symptomatic of an unsettling property of program analyses: their quality is unpredictably vulnerable to syntactic accidents in source programs, i.e., to the way these programs are written. More reliable program analyses require a better understanding of the effect of syntactic change.

A string-formatting function such as printf in C seemingly requires dependent types, because its control string determines the rest of its arguments. Examples: formula here We show how changing the representation of the control string makes it possible to program printf in ML (which does not allow dependent types). The result is well typed and perceptibly more efficient than the corresponding library functions in Standard ML of New Jersey and in Caml.

Lambda-lifting a functional program transforms it into a set of recursive equations. We present the symmetric transformation: lambda-dropping. Lambda-dropping a set of recursive equations restores block structure and lexical scope.For lack of scope, recursive equations must carry around all the parameters that any of their callees might possibly need. Both lambda-lifting and lambda-dropping thus require one to compute a transitive closure over the call graph:• for lambda-lifting: to establish the Def/Use path of each free variable (these free variables are then added as parameters to each of the functions in the call path);• for lambda-dropping: to establish the Def/Use path of each parameter (parameters whose use occurs in the same scope as their definition do not need to be passed along in the call path).Without free variables, a program is scope-insensitive. Its blocks are then free to float (for lambda-lifting) or to sink (for lambda-dropping) along the vertices of the scope tree.We believe lambda-lifting and lambda-dropping are interesting per se, both in principle and in practice, but our prime application is partial evaluation: except for Malmkjær and Ørbæk's case study presented at PEPM '95, most polyvariant specializers for procedural programs operate on recursive equations. To this end, in a pre-processing phase, they lambda-lift source programs into recursive equations, As a result, residual programs are also expressed as recursive equations, often with dozens of parameters, which most compilers do not handle efficiently. Lambda-dropping in a post-processing phase restores their block structure and lexical scope thereby significantly reducing both the compile time and the run time of residual programs.

Thirty-five years ago, thunks were used to simulate call-by-name under call-by-value in Algol 60. Twenty years ago, Plotkin presented continuation-based simulations of call-by-name under call-by-value and vice versa in the λ-calculus. We connect all three of these classical simulations by factorizing the continuation-based call-by-name simulation [Cscr ]n with a thunk-based call-by-name simulation [Tscr ] followed by the continuation-based call-by-value simulation [Cscr ]v, extended to thunks.formula hereWe show that [Tscr ] actually satisfies all of Plotkin's correctness criteria for [Cscr ]n (i.e. his Indifference, Simulation and Translation theorems). Furthermore, most of the correctness theorems for [Cscr ]n can now be seen as simple corollaries of the corresponding theorems for [Cscr ]v and [Tscr ].

We formalize a partial evaluator for Eugenio Moggi's computational metalanguage. This formalization gives an evaluation-order independent view of binding-time analysis and program specialization, including a proper treatment of call unfolding. It also enables us to express the essence of ‘control-based binding-time improvements’ for let expressions. Specifically, we prove that the binding-time improvements given by ‘continuation-based specialization’ can be expressed in the metalanguage via monadic laws.

We present a strikingly simple partial evaluator, that is type-directed and reifies a compiled program into the text of a residual, specialized program. Our partial evaluator is concise (a few lines) and it handles the flagship examples of offline monovariant partial evaluation. Its source programs are constrained in two ways: they must be closed and monomorphically typable. Thus dynamic free variables need to be factored out in a "dynamic initial environment". Type-directed partial evaluation uses no symbolic evaluation for specialization, and naturally processes static computational effects.Our partial evaluator is the part of an offline partial evaluator that residualizes static values in dynamic contexts. Its restriction to the simply typed lambda-calculus coincides with Berger and Schwichtenberg's "inverse of the evaluation functional" (LICS'91), which is an instance of normalization in a logical setting. As such, type-directed partial evaluation essentially achieves lambda-calculus normalization. We extend it to produce specialized programs that are recursive and that use disjoint sums and computational effects. We also analyze its limitations: foremost, it does not handle inductive types.This paper therefore bridges partial evaluation and λ-calculus normalization through higher-order abstract syntax, and touches upon parametricity, proof theory, and type theory (including subtyping and coercions), compiler optimization, and rut-time code generation (including decompilation). It also offers a simple solution to denotational semantics-based compilation and compiler generation.

Partial-evaluation folklore has it that massaging one's source programs can make them specialize better. In Jones, Gomard, and Sestoft's recent textbook, a whole chapter is dedicated to listing such “binding-time improvements”: nonstandard use of continuation-passing style, eta-expansion, and a popular transformation called “The Trick.” We provide a unified view of these binding-time improvements, from a typing perspective. Just as a proper treatment of product values in partial evaluation requires partially static values, a proper treatment of disjoint sums requires moving static contexts across dynamic case expressions. This requirement precisely accounts for the nonstandard use of continuation-passing style encountered in partial evaluation. Eta-expansion thus acts as a uniform binding-time coercion between values and contexts, be they of function type, product type, or disjoint-sum type. For the latter case, it enables “The Trick.” In this article, we extend Gomard and Jones' partial evaluator for the λ-calculus, λ-Mix, with products and disjoint sums; we point out how eta-expansion for (finite) disjoint sums enable The Trick; we generalize our earlier work by identifying the eta-expansion can be obtained in the binding-time analysis simple by adding two coercion rules; and we specify and prove the correctness of our extension to λ-Mix.

We unify previous work on the continuation-passing style (CPS) transformations in a generic framework based on Moggi's computational met a-language.This framework is used to obtain GPS transformations for a variety of evaluation strategies and to characterize the corresponding administrative reductions and inverse transformations.We establish generic formal connections between operational semantics and equational theories.Formal properties of transformations for specific evaluation orders follow as corollaries.Essentially, we factor transformations through Moggi's computational meta-language.Mapping A-terms into the met a-language captures computational properties (e.g., partiality, strictness) and evaluation order explicitly in both the term and the type structure of the meta-language.The CPS transformation is then obtained by applying a generic transformation from terms and types in the meta-language to CPS terms and types, based on a typed term representation of the continuation monad.We prove an adequacy property for the generic transformation and establish an equational correspondence between the meta-language and CPS terms.These generic results generalize Plotkin's seminal theorems, subsume more recent results, and enable new uses of CPS transformations and their inverses.We discuss how to apply these results to compilation.

The last years have witnessed a flurry of new results in the area of partial evaluation. These tutorial notes survey the field and present a critical assessment of the state of the art.

The continuation-passing style (CPS) transformation is powerful but complex. Our thesis is that this transformation is in fact compound, and we set out to stage it. We factor the CPS transformation into several steps, separating aspects in each step: (1) Intermediate values are named; (2) Continuations are introduced; (3) Sequencing order is decided and administrative reductions are performed.

This paper investigates the transformation of λ ν -terms into continuation-passing style (CPS). We show that by appropriate η-expansion of Fisher and Plotkin's two-pass equational specification of the CPS transform, we can obtain a static and context-free separation of the result terms into “essential” and “administrative” constructs. Interpreting the former as syntax builders and the latter as directly executable code, We obtain a simple and efficient one-pass transformation algorithm, easily extended to conditional expressions, recursive definitions, and similar constructs. This new transformation algorithm leads to a simpler proof of Plotkin's simulation and indifference results. We go on to show how CPS-based control operators similar to, more general then, Scheme's call/cc can be naturally accommodated by the new transformation algorithm. To demonstrate the expressive power of these operators, we use them to present an equivalent but even more concise formulation of the efficient CPS transformation algorithm. Finally, we relate the fundamental ideas underlying this derivation to similar concepts from other work on program manipulation; we derive a one-pass CPS transformation of λ n -terms; and we outline some promising areas for future research.

This paper presents a step forward in the use of partial evaluation for interpreting and compiling programs, as well as for automatically generating a compiler from denotational definitions of programming languages. We determine the static and dynamic semantics of a programming language, reduce the expressions representing the static semantics, and generate object code by instantiating the expressions representing the dynamic semantics. By processing the static semantics of the language, programs get compiled. By processing the static semantics of the partial evaluator, compilers are generated. The correctness of a compiler is guaranteed by the correctness of both the executable specification and our partial evaluator. The results reported in this paper improve on previous work in the domain of compiler generation [16, 30], and solves several open problems in the domain of partial evaluation [15]. In essence: ffl Our compilation goes beyond a mere syntax-tosemantics mapping since the ...

This paper presents a constant-time marking-collecting algorithm to efficiently implement recursion with a general heap memory rather than with a vectorial stack, in a context of frequent captures of continuations. It has been seen to reduce the 80% garbage collection overhead to less than 5% on average.The algorithm has been built into a virtual machine to efficiently implement at the assembly level the Actor language PLASMA, an Actor-oriented version of PROLOG and a variant of SCHEME, currently in use on 8086, 68000 and Vax.The rationale to use the heap memory is that continuations are available via a single pointer in a unified memory and can be shared optimally when recurrently captured, which is simply impossible using a strategy based on stack recopy. Further, non-captured continuations can be incrementally garbage collected on the fly.Part I describes the elementary recursive instructions of the virtual machine. Part II presents and proves the marking-collecting strategy. Part III safely generalizes the transformation "call + return = branch" in a way compatible with the possible capture of the current continuation. An appendix relates its integration in the Virtual Scheme Machine supporting Scheme 84.