A unifying approach to goal-directed evaluation.
Goal-directed evaluation, as embodied in Icon and Snobol, is built on the notions of backtracking and of generating successive results, and therefore it has always been something of a challenge to specify and implement. In this article, we address this challenge using computational monads and partial evaluation.We consider a subset of Icon and we specify it with a monadic semantics and a list monad. We then consider a spectrum of monads that also fit the bill, and we relate them to each other. For example, we derive a continuation monad as a Church encoding of the list monad. The resulting semantics coincides with Gudeman's continuation semantics of Icon.We then compile Icon programs by specializing their interpreter (i.e., by using the first Futamura projection), using type-directed partial evaluation. Through various back ends, including a run-time code generator, we generate ML code, C code, and OCaml byte code. Binding-time analysis and partial evaluation of the continuation-based interpreter automatically give rise to C programs that coincide with the result of Proebsting's optimized compiler.
Introduction
Goal-directed languages combine expressions that can yield multiple results
through backtracking. Results are generated one at a time: an expression can
either succeed and generate a result, or fail. If an expression fails, control is
passed to a previous expression to generate the next result, if any. If so, control
is passed back to the original expression in order to try whether it can succeed
this time. Goal-directed programming specifies the order in which subexpressions
are retried, thus providing the programmer with a succint and powerful
control-flow mechanism. A well-known goal-directed language is Icon [11].
Backtracking as a language feature complicates both semantics and imple-
mentation. Gudeman [13] gives a continuation semantics of a goal-directed
language; continuations have also been used in implementations of languages
with control structures similar to those of goal-directed evaluation, such as Prolog
[3, 15, 30]. Proebsting and Townsend, the implementors of an Icon compiler
in Java, observe that continuations can be compiled into e#cient code [1, 14],
but nevertheless dismiss them because "[they] are notoriously di#cult to under-
stand, and few target languages directly support them" [23, p.38]. Instead, their
compiler is based on a translation scheme proposed by Proebsting [22], which
is based on the four-port model used for describing control flow in Prolog [2].
Icon expressions are translated to a flow-chart language with conditional, direct
and indirect jumps using templates; a subsequent optimization which, amongst
other things, reorders code and performs branch chaining, is necessary to produce
compact code. The reference implemention of Icon [12] compiles Icon into
byte code; this byte code is then executed by an interpreter that controls the
control flow by keeping a stack of expression frames.
In this article, we present a unified approach to goal-directed evaluation:
1. We consider a spectrum of semantics for a small goal-directed language.
We relate them to each other by deriving semantics such as Gudeman's [13]
as instantiations of one generic semantics based on computational monads
[21]. This unified approach enables us to show the equivalence of
di#erent semantics simply and systematically. Furthermore, we are able
to show strong conceptual links between di#erent semantics: Continuation
semantics can be derived from semantics based on lists or on streams of
results by Church-encoding the lists or the streams, respectively.
2. We link semantics and implementation through semantics-directed compilation
using partial evaluation [5, 17]. In particular, binding-time analysis
guides us to extract templates from the specialized interpreters. These
templates are similar to Proebsting's, and through partial evaluation, they
give rise to similar flow-chart programs, demonstrating that templates are
not just a good idea-they are intrinsic to the semantics of Icon and can
be provably derived.
The rest of the paper is structured as follows: In Section 2 we first describe
syntax and monadic semantics of a small subset of Icon; we then instantiate the
semantics with various monads, relate the resulting semantics to each other, and
present an equivalence proof for two of them. In Section 3 we describe semantics-
directed compilation for a goal-directed language. Section 4 concludes.
2 Semantics of a Subset of Icon
An intuitive explanation of goal-directed evaluation can be given in terms of lists
and list-manipulating functions. Consequently, after introducing the subset of
Icon treated in this paper, we define a monadic semantics in terms of the list
monad. We then show that also a stream monad and two di#erent continuation
monads can be used, and we give an example of how to prove equivalence of the
resulting monads using a monad morphism.
2.1 A subset of the Icon programming language
We consider the following subset of Icon:
Intuitively, an Icon term either fails or succeeds with a value. If it succeeds, then
subsequently it can be resumed, in which case it will again either succeed or fail.
This process ends when the expression fails. Informally, i succeeds with the value
succeeds with the sum of the sub-expressions; E 1 to E 2 (called a
succeeds with the value of E 1 and each subsequent resumption yields
the rest of the integers up to the value of E 2 , at which point it
succeeds with the value of E 2 if it is larger than the value
produces the results of
it produces the results of E 3 .
Generators can be nested. For example, the Icon term 4 to (5 to 7) generates
the result of the expressions 4 to 5, 4 to 6, and 4 to 7 and concatenates
the results.
In a functional language such as Scheme, ML or Haskell, we can achieve the
e#ect of Icon terms using the functions map and concat. For example, if we
define
fun to
in ML, then evaluating concat (map (to
6, 4, 5, 6, 7] which is the list of the integers produced by the Icon term 4
to (5 to 7).
2.2 Monads and semantics
Computational monads were introduced to structure denotational semantics [21].
The basic idea is to parameterize a semantics over a monad; many language ex-
tensions, such as adding a store or exceptions, can then be carried out by simply
instantiating the semantics with a suitable monad. Further, correspondence
join M

Figure

1: Monad operators and their types
Standard monad operations:
unit
join L
join L
(l
Special operations for sequences:
empty
if empty L [
if empty L
append L

Figure

2: The list monad
proofs between semantics arising from instantiation with di#erent monads can
be conducted in a modular way, using the concept of a monad morphism [28].
Monads can also be used to structure functional programs [29]. In terms of
programming languages, a monad M is described by a unary type constructor
M and three operations unit M , map M
and join M
with types as displayed in

Figure

1. For these operations, the so-called monad laws have to hold.
In Section 2.4 we give a denotational semantics of the goal-directed language
described in Section 2.1. Anticipating semantics-directed compilation by partial
evaluation, we describe the semantics in terms of ML, in e#ect defining an
interpreter. The semantics int M is parameterized over a monad
M, where #M represents a sequence of values of type #.
where
(#x.join M
to
else append M (unit M i) (to M (i

Figure

3: Monadic semantics for a subset of Icon
2.3 A monad of sequences
In order to handle sequences, some structure is needed in addition to the three
generic monad operations displayed in Figure 1. We add three operations:
empty M
append M
Here, empty M stands for the empty sequence; if empty M is a discriminator
function that, given a sequence and two additional inputs, returns the first
input if the sequence is empty, and returns the second input otherwise; append M
appends two sequences.
A straightforward instance of a monad of sequences is the list monad L,
which is displayed in Figure 2; for lists, "join" is sometimes also called "flatten"
or, in ML, "concat".
2.4 A monadic semantics
A monadic semantics of the goal-directed language described in Section 2.1. is
given in Figure 3. We explain the semantics in terms of the list monad. A literal
i is interpreted as an expression that yields exactly one result; consequently, i is
mapped into the singleton list [i] using unit . The semantics of to, + and <= are
given in terms of bind2 and a function of type int # int # int list. The type of
function bind2 L is
list # list # list,
i.e., it takes two lists containing values of type # and #, and a function mapping
# into a list of values of type #. The e#ect of the definition of bind2 L f xs ys
is (1) to map f x over ys for each x in xs and (2) to flatten the resulting list of
lists. Both steps can be found in the example at the end of Section 2.1 of how
the e#ect of goal-directed evaluation can be achieved in ML using lists.
2.5 A spectrum of semantics
In the following, we describe four possible instantiations of the semantics given
in

Figure

3. Because a semantics corresponds directly to an interpreter, we thus
create four di#erent interpreters.
2.5.1 A list-based interpreter
Instantiating the semantics with the list monad from Figure 2 yields a list-based
interpreter. In an eager language such as ML, a list-based interpreter always
computes all results. Such behavior may not be desirable in a situation where
only the first result is of interest (or, for that matter, whether there exists a
result): Consider for example the conditional, which examines whether a given
expression yields at least one result or fails. An alternative is to use laziness.
2.5.2 A stream-based interpreter
Implementing the list monad from Figure 2 in a lazy language results in a monad
of (finite) lazy lists; the corresponding interpreter generates one result at a time.
In an eager language, this e#ect can be achieved by explicitly implementing a
data type of streams, i.e., finite lists built lazily: a thunk is used to delay
computation.
The definition of the corresponding monad operations is straightforward.
2.5.3 A continuation-based interpreter
Gudeman [13] gives a continuation-based semantics of a goal-directed language.
We can derive this semantics by instantiating our monadic semantics with the
continuation monad C as defined in Figure 4. The type-constructor #C of the
continuation monad is defined as (# R) # R, where R is called the answer
type of the continuation.
A conceptual link between the list monad and the continuation monad with
answer type # list # list can be made through a Church encoding [4] of the
higher-order representation of lists proposed by Hughes [16]. Hughes observed
that when constructing the partially applied concatenation function #ys .xs @ ys
rather than the list xs , lists can be appended in constant time. In the resulting
representation, the empty list corresponds to the function that appends no ele-
ments, i.e., the identity, whereas the function that appends a single element is
Standard monad operations:
unit
join
Special operations for sequences:
empty C
if empty C
xs ys
append C

Figure

4: The continuation monad
represented by a partially applied cons function:
cons
Church-encoding a data types means abstracting over selector functions, in this
case " :: ":
cons
The resulting representation of lists can be typed as
(#,
which indeed corresponds to #C with answer type #. Notice that nil and
cons for this list representation yield empty C and unit C , respectively. Similarly,
the remaining monad operations correspond to the usual list operations.

Figure

5 displays the definition of operations have been
inlined and the resulting expressions #-reduced.
2.5.4 An interpreter with explicit success and failure continuations
A tail-recursive implementation of a continuation-based interpreter for Icon uses
explicit success and failure continuations. The result of interpreting an Icon
expression then has type
(int
where the first argument is the success continuation and the second argument
the failure continuation. Note that the success continuation takes a failure continuation
as a second argument. This failure continuation determines the resumption
behavior of the Icon term: the success continuation may later on apply
where
to C
else

Figure

5: A continuation semantics
its failure continuation to generate more results. The corresponding continuation
monad C 2 has the same standard monad operations as the continuation
monad displayed in Figure 4, and the sequence operations
empty
if empty C 2
xs ys
append
Just as the continuation monad from Figure 4 can be conceptually linked to the
list monad, the present continuation monad can be linked to the stream monad
by a Church encoding of the data type of streams:
more x
The fact that the second component in a stream is a thunk suggests one to give
the selector function s m the type int # (1 1 1 #; the resulting type for end
and more x xs is then
(int
Choosing # as the result type of the selector functions yields the type of a
continuation monad with answer type
The interpreter defined by the semantics
is the starting point of the
semantics-directed compilation described in Section 3. Figure 6 displays the
definition of
where all monad operations have been inlined and the resulting
expressions #-reduced. Because the basic monad operations of C 2 are the same
as those of C, the semantics based on C 2 and C only di#er in the definitions of
leq , to , and in how if is handled.
(#j.to
where
to C 2
else

Figure

A semantics with success and failure continuations
2.6 Correctness
So far, we have related the various semantics presented in Section 2.5 only con-
ceptually. Because the four di#erent interpreters presented in Section 2.5 were
created by instantiating one parameterized semantics with di#erent monads, a
formal correspondence proof can be conducted in a modular way building on
the concept of a monad morphism [28].
and N are two monads, then h :
#M #N is a monad morphism if it preserves the monad operations 1 , i.e.,
The following lemma shows that the semantics resulting from two di#erent
monad instantiations can be related by defining a monad morphism between
the two sequence monads in question.
and N be monads of sequences as specified in Section 2.3. If
h is a monad morphism from M to N, then for every Icon
expression E.
We strengthen the definition of a monad morphism somewhat by considering a sequence-
preserving monomorphism that also preserves the monad operations specific to the monad of
sequences.
Proof: By induction over the structure of E. A lemma to the e#ect that
shown by induction over
We use Lemma 2 to show that the list-based interpreter from Section 2.5.1 and
the continuation-based interpreter from Section 2.5.3 always yield comparable
results:
Proposition 3 Let show : #C # L be defined as
show
(unit L x) xs) empty L .
Then (show expressions E.
Proof: We show that (1) h : # L #C, which is defined as
(unit C x) (h xs)
is a monad morphism from L to C, and (2) the function (show #h) is the identity
function on lists. The proposition then follows immediately with Lemma 2. #
2.7 Conclusion
Taking an intuitive list-based semantics for a subset of Icon as our starting point,
we have defined a stream-based semantics and two continuation semantics. Because
our inital semantics is defined as the instantiation of a monadic semantics
with a list monad, the other semantics can be defined through a stream monad
and two di#erent continuation monads, respectively. The modularity of the
monadic semantics allows us to relate the semantics to each other by relating
the corresponding monads, both conceptually and formally. To the best of
our knowledge, the conceptual link between list-based monads and continuation
monads via Church encoding has not been observed before.
It is known that continuations can be compiled into e#cient code relatively
easily [1, 14]; in the following section we show that partial evaluation is su#-
cient to generate e#cient code from the the continuation semantics derived in
Section 2.5.4.
3 Semantics-Directed Compilation
The goal of partial evaluation is to specialize a source program
of two arguments to a fixed "static" argument s : S. The result is a residual
program that must yield the same result when applied to a "dy-
namic" argument d as the original program applied to both the static and the
dynamic arguments, i.e., [[p s
Our interest in partial evaluation is due to its use in semantics-directed com-
pilation: when the source program p is an interpreter and the static argument s
is a term in the domain of p then p s is a compiled version of s represented in the
implementation language of p. It is often possible to implement an interpreter
in a functional language based on the denotational semantics.
Our starting point is a functional interpreter implementing the denotational
semantics in Figure 6. The source language of the interpreter is shown in Figure
7. In Section 3.1 we present the Icon interpreter written in ML. In Section
3.1, 3.2, and 3.3 we use type-directed partial evaluation to specialize this
interpreter to Icon terms yielding ML code, C code, and OCaml byte code as
output. Other partial-evaluation techniques could be applied to yield essentially
the same results.
structure struct
datatype
| TO of icon * icon
| PLUS of icon * icon
| LEQ of icon * icon
| IF of icon * icon * icon

Figure

7: The abstract syntax of Icon terms
3.1 Type-directed partial evaluation
We have used type-directed partial evaluation to compile Icon programs into
ML. This is a standard exercise in semantics-directed compilation using type-directed
partial evaluation [9].
Type-directed partial evaluation is an approach to o#-line specialization of
higher-order programs [8]. It uses a normalization function to map the (value of
trivially specialized program #d.p(s, d) into the (text of the) target program
The input to type-directed partial evaluation is a binding-time separated program
in which static and dynamic primitives are separated. When implemented
in ML, the source program is conveniently wrapped in a functor parameterized
over a structure of dynamic primitives. The functor can be instantiated with
evaluating primitives (for running the source program) and with residualizing
primitives (for specializing the source program).
3.1.1 Specializing Icon terms using type-directed partial evaluation
In our case the dynamic primitives operations are addition (add), integer comparison
(leq), a fixed-point operator (fix), a conditional functional (cond), and
a quoting function (qint) lifting static integers into the dynamic domain. The
signature of primitives is shown in Figure 8. For the residualizing primitives
we let the partial evaluator produce functions that generate ML programs with
meaningful variable names [8].
The parameterized interpreter is shown in Figure 9. The main function eval
takes an Icon term and two continuations, res
res, and yields a result of type res. We intend to specialize
the interpreter to a static Icon term and keeping the continuation parameters
k and f dynamic. Consequently, residual programs are parameterized over two
continuations. (If the continuations were also considered static then the residual
programs would simply be the list of the generated integers.)
signature
type tunit
type tint
type tbool
type res
val qint : int -> tint
val add : tint * tint -> tint
res
val fix : ((tint -> res) -> tint -> res) -> tint -> res

Figure

8: Signature of primitive operations
The output of type-directed partial evaluation is the text of the residual
program. The residual program is in long beta-eta normal form, that is, it does
not contain any beta redexes and it is fully eta-expanded with respect to its
type.
Example 4 The following is the result of specializing the interpreter with respect
to the Icon (4 to 7).
fix (fn loop0 =>
fn i0 =>
cond (leq (i0, qint 7),
(fn () => loop0 (add (i0, qint 1))),
(qint
struct
fun loop (i,
P.fix
(fn walk =>
P.cond (P.leq (i, j),
fn _ =>
walk (P.add (i, P.qint 1))),
fun select (i,
P.cond (P.leq (i, j), fn _ => k j f, f)
fun sum (i,
fun eval (LIT i)
| eval (TO(e1,
eval e1 (fn i => eval e2 (fn j => loop (i,
| eval (PLUS(e1,
eval e1 (fn i => eval e2 (fn j => sum (i,
| eval (LEQ(e1,
eval e1 (fn i => eval e2 (fn j => select (i,
| eval (IF(e1, e2,
eval e1
(fn _ => fn _ => eval e2 k f)
(fn _ => eval e3 k f)

Figure

9: Parameterized interpreter
3.1.2 Avoiding code duplication
The result of specializing the interpreter in Figure 9 may be exponentially large.
This is due to the continuation parameter k being duplicated in the clause for
IF. For example, specializing the interpreter to the Icon term 100
yields the following residual program in which the context
cond (leq (qint 1, qint 2),
Code duplication is a well-known problem in partial evaluation [17]. The
equally well-known solution is to bind the continuation in the residual program,
just before it is used. We introduce a new primitive save of two arguments, k
and g, which applies g to two "copies" of the continuation k.
signature
res
val save : succ -> (succ * succ -> res) -> res
The final clause of the interpreter is modified to save the continuation parameter
before it proceeds, as follows.
fun eval (LIT i)
| eval (IF(e1, e2,
save k
(fn (k0, k1) => eval e1
(fn _ => fn _ => eval e2 k0 f)
(fn _ => eval e3 k1 f))
Specializing this new interpreter to the Icon term from above yields the
following residual program in which the context add(100, - ) occurs only once.
save (fn v0 =>
fn resume0 =>
k (add (qint 100, v0)) (fn () => resume0 ()))
(fn (k0_0, k1_0) =>
cond (leq (qint 1, qint 2),
Two copies of continuation parameter k are bound to k0 0 and k1 0 before the
continuation is used (twice, in the body of the second lambda). In order just to
prevent code duplication, passing one "copy" of the continuation parameter is
actually enough. But the translation into C introduced in Section 3.2 uses the
two di#erently named variables, in this case k0_0 and k1_0, to determine the
IF-branch inside which a continuation is applied.
3.2 Generating C programs
Residual programs are not only in long beta-eta normal form. Their type
(tint # (tunit # res) # res) # (tunit # res) # res
imposes further restrictions: A residual program must take two arguments, a
success continuation res and a failure continuation
res, and it must produce a value of type res. When we also
consider the types of the primitives that may occur in residual programs we see
that values of type res can only be a result of
. applying the success continuation k to an integer n and function of type
tunit # res;
. applying the failure continuation f;
. applying the primitive cond to a boolean and two functions of type tunit #
res;
. applying the primitive fix to a function of two arguments, loop n
res and in : tint, and an integer;
. (inside a function passed to fix) applying the function loop n
to an integer;
. applying the primitive save to two arguments, the first being a function
of two arguments, vn : tint and resumen : tunit # res, and the second
being a function of a pair of arguments, k 0
, each of type tint #
(tunit # res) # res;
. (inside the first function passed to save) applying the function resumen ;
or
. (inside the second function passed to save) applying one of the functions
n to an integer and a function of type tunit # res.
A similar analysis applies to values of type tint: they can only arise from
evaluating an integer n, a variable in , or a variable vn or from applying add to
two argument of type tint. As a result, we observe that the residual programs
of specializing the Icon interpreter using type-directed partial evaluation are
restricted to the grammar in Figure 10. (The restriction that the variables
loop n
, in , vn , and resume n each must occur inside a function that binds them
cannot be expressed using a context-free grammar. This is not a problem for our
development.) We have expressed the grammar as an ML datatype and used this
datatype to represent the output from type-directed partial evaluation. Thus,
we have essentially used the type system of ML as a theorem prover to show
the following lemma.
Lemma 5 The residual program generated from applying type-directed partial
evaluation to the interpreter in Figure 9 can be generated by the grammar in

Figure

10.
The idea of generating grammars for residual programs has been studied by,
e.g., Malmkj-r [20] and is used in the run-time specializer Tempo to generate
code templates [6].
| f ()
| cond (E, fn () => S, fn () => S)
| fix (fn loop n => fn in => S) E
| loop n E
| save (fn vn => fn resumen =>
| resume n ()
in | vn | add (E, E) | leq (E, E)

Figure

10: Grammar of residual programs
The simple structure of output programs allows them to be viewed as programs
of a flow-chart language. We choose C as a concrete example of such a
language. Figure 11 and 12 show the translation from residual programs to C
programs.
The translation replaces function calls with jumps. Except for the call to
resume n (which only occurs as the result of compiling if-statements), the name
of a function uniquely determines the corresponding label to jump to. Jumps to
resume n can end up in two di#erent places corresponding to the two copies of
the continuation. We use a boolean variable gate n
to distinguish between the
two possible destinations. Calls to loop n
and kn pass arguments. The names
of the formal parameters are known (i n and vn , respectively) and therefore
arguments are passed by assigning the variable before the jump.
In each translation of a conditional a new label l must be generated. The
entire translated term must be wrapped in a context that defines the labels succ
and fail (corresponding to the initial continuations). The statements following
the label succ are allowed to jump to resume. The translation in Figure 11 and
12 generates a C program that successively prints the produced integers one by
one. A lemma to the e#ect that the translation from residual ML programs into
C is semantics preserving would require giving semantics to C and to the subset
of ML presented in Figure 10 and then showing equivalence.
Example 6 Consider again the Icon (4 to 7) from Example 4. It
is translated into the following C program.
loop0: if (i0 <= 7) goto L0;
goto fail;
goto succ;
| S
succ: printf("%d ", value);
goto resume;
goto succ;
resume: |S| S
|f
|cond (E, fn () => S, fn () => S # )|
if (|E| E) goto l;
l: |S| S
|fix (fn loop n => fn in => S) E|
goto loop
save (fn vn => fn resumen => S)
succn: |S| S
|resumen
goto resume 0
gate
goto
resume i

Figure

Translating residual programs into C (Statements)
|qint

Figure

12: Translating residual programs into C (Expressions)
resume:
goto loop0;
succ: printf("%d ", value);
goto resume;
The C target programs corresponds to the target programs of Proebsting's
optimized template-based compiler [22]. In e#ect, we are automatically generating
flow-chart programs from the denotation of an Icon term.
3.3 Generating byte code
In the previous two sections we have developed two compilers for Icon terms,
one that generates ML programs and one that generates flow-chart programs.
In this section we unify the two by composing the first compiler with the third
author's automatic run-time code generation system for OCaml [25] and by
composing the second compiler with a hand-written compiler from flow charts
into OCaml byte code.
3.3.1 Run-time code generation in OCaml
Run-time code generation for OCaml works by a deforested composition of traditional
type-directed partial evaluation with a compiler into OCaml byte code.
Deforestation is a standard improvement in run-time code generation [6, 19, 26].
As such, it removes the need to manipulate the text of residual programs at specialization
time. As a result, instead of generating ML terms, run-time code generation
allows type-directed partial evaluation to directly generate executable
OCaml byte code.
Specializing the Icon interpreter from Figure 9 to the Icon
to 7) using run-time code generation yields a residual program of about 110
byte-code instructions in which functions are implemented as closures and calls
are implemented as tail-calls. (Compiling the residual ML program using the
OCaml compiler yields about 90 byte-code instructions.)
3.3.2 Compiling flow charts into OCaml byte code
We have modified the translation in Figure 11 and 12 to produce OCaml byte-code
instructions instead of C programs. The result is an embedding of Icon
into OCaml.
Using this (4 to 7) yields 36 byte-code instructions in which
functions are implemented as labelled blocks and calls are implemented as an
assignment (if an argument is passed) followed by a jump. This style of target
code was promoted by Steele in the first compiler for Scheme [27].
3.4 Conclusion
Translating the continuation-based denotational semantics into an interpreter
written in ML and using type-directed partial evaluation enables a standard
semantics-directed compilation from Icon terms into ML. A further compilation
of residual programs into C yields flow-chart programs corresponding to those
produced by Proebsting's Icon compiler [22].
4 Conclusions and Issues
Observing that the list monad provides the kind of backtracking embodied in
Icon, we have specified a semantics of Icon that is parameterized by this monad.
We have then considered alternative monads and proven that they also provide
a fitting semantics for Icon. Inlining the continuation monad, in particular,
yields Gudeman's continuation semantics [13].
Using partial evaluation, we have then specialized these interpreters with
respect to Icon programs, thereby compiling these programs using the first Futamura
projection. We used a combination of type-directed partial evaluation
and code generation, either to ML, to C, or to OCaml byte code. Generating
code for C, in particular, yields results similar to Proebsting's compiler [22].
Gudeman [13] shows that a continuation semantics can also deal with additional
control structures and state; we do not expect any di#culties with scaling
up the code-generation accordingly. The monad of lists, on the other hand, does
not o#er enough structure to deal, e.g., with state. It should be possible, how-
ever, to create a rich enough monad by combining the list monad with other
monads such as the state monad [10, 18].
It is our observation that the traditional (in partial evaluation) generalization
of the success continuation avoids the code duplication that Proebsting
presents as problematic in his own compiler. We are also studying the results
of defunctionalizing the continuations, -a la Reynolds [24], to obtain stack-based
specifications and the corresponding run-time architectures.

Acknowledgments

Thanks are due to the anonymous referees for comments
and to Andrzej Filinski for discussions. This work is supported by the ESPRIT
Working Group APPSEM (http://www.md.chalmers.se/Cs/Research/
Semantics/APPSEM/).



--R

Compiling with Continuations.
Understanding the control of Prolog programs.
On implementing Prolog in functional programming.
The Calculi of Lambda-Conversion
Tutorial notes on partial evalua- tion
A general approach for run-time specialization and its application to C



Representing layered monads.
The Icon Programming Lan- guage
The Implementation of the Icon Programming Language.
Denotational semantics of a goal-directed language
Representing control in the presence of first-class continuations
Prological features in a functional setting-axioms and implementations
"reverse"
Partial Evaluation and Automatic Program Generation.
Combining Monads.
Optimizing ML with run-time code generation
Abstract Interpretation of Partial-Evaluation Algo- rithms
Computational lambda-calculus and monads
Simple translation of goal-directed evaluation
A new implementation of the Icon language.
Definitional interpreters for higher-order programming languages
PhD thesis
Two for the price of one: composing partial evaluation and compilation.
Steele Jr.
Comprehending monads.
Monads for functional programming.
An easy implementation of pil (PROLOG in LISP).
--TR
A novel representation of lists and its application to the function "reverse"
The implementation of the Icon programming language
Computational lambda-calculus and monads
Representing control in the presence of first-class continuations
Denotational semantics of a goal-directed language
Compiling with continuations
Partial evaluation and automatic program generation
Tutorial notes on partial evaluation
Optimizing ML with run-time code generation
A general approach for run-time specialization and its application to C
Representing layered monads
ICON Programmng Language
Definitional Interpreters for Higher-Order Programming Languages
Type-Directed Partial Evaluation
Semantics-Based Compiling
Combining Monads
Monads for Functional Programming

--CTR
Mitchell Wand , Dale Vaillancourt, Relating models of backtracking, ACM SIGPLAN Notices, v.39 n.9, September 2004
Dariusz Biernacki , Olivier Danvy , Chung-chieh Shan, On the static and dynamic extents of delimited continuations, Science of Computer Programming, v.60 n.3, p.274-297, May 2006
continuations;evaluation computational monads;run-time code generation;code templates;type-directed partial evaluation