An Approach to Call-by-Name Delimited Continuations
---------------------------------------------------
Errata to the POPL version
--------------------------
1- Incorrect rephrasing of David and Py's and of Saurin's separability results
The notion of normal forms up to equalities used in the reformulation
of Saurin's separability result (Theorem 2) does not faithfully
rephrase the original formulation (and moreover, the modified
statement is wrong). Rephrase Theorem 2 as follows:
Theorem 2 (Saurin 2005). A normal term is called canonical if it
contains no subterms of the form [alpha]\x.M. Now, if the closed
canonical normal terms M and N in Lambda-mu are not equated by the
equational theory in Figure 2 then they are separable, i.e., for any
two variables x and y, there exists a context D_n, such that D_n[M] =
x and D_n[N] = y.
The same remark applies to Corollary 12 which has to be rephrased as
follows:
Corollary 12. Call-by-name lambda-mu-tp-hat is observationally
complete for closed canonical normal forms: Calling a normal form
canonical if it contains no subterms of the form [alpha]\l x.M, we have
that for any closed canonical normal forms M and N not equal in
call-by-name lambda-mu-tp-hat, there exists an evaluation context D_n,
such that, mu tp-hat.D_n[[tp-hat]M] = x and mu tp-hat.D_n[[tp-hat]N] = y
for x and y arbitrary fresh variables.
To faithfully cite David and Py's non separability result, Theorem 1
should also be changed (even it the version stated in the paper is
correct) into:
A normal term is called {\em canonical} if it contains no subterms of
the form [\alpha]\x.M. There are two closed canonical normal terms
W_0 and W_1 that are not equated by the equational theory in Figure 1
and of which the observational behaviour is not separable, i.e., for
distinct fresh variables x and y, there is no applicative context E_n,
such that E_n[W_0] = x and E_n[W_1] = y.
2- Incorrect claim about typed de Groote calculus
The statement asserting in the introduction that the typed version of
the calculus defined by de Groote's in LPAR 1994 is equivalent to
Parigot's lambda-mu extended with a continuation variable tp of type
bottom is wrong. A correct statement is:
The calculus defined by de Groote's in LPAR 1994, _and_ equipped with
rule (epsilon), as in de Groote's paper MCSC 1998, is equivalent to
Parigot's lambda-mu extended with a continuation variable tp of type
bot.
3- Typo: on page 8, just before Proposition 16, the translation of
"Delta, alpha:A" is "Delta^-, k_alpha:A^-" instead of "Delta^-, alpha:A^-".