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^-".