A Type-Theoretic Foundation of Continuations and Prompts (erratum) ------------------------------------------------------------------ Proposition 8 is wrong as stated because the translation of (tp-hat M) is not stable under reduction due to the outer occurrence of tp in tp(join M^tp) being locally bound instead of globally. It can be fixed in at least two different ways. 1) Define an equivalence ~~ collapsing all terms which differs only by the choice of where tp is bound in subexpressions of the form "tp(join M)". This allows to restate Proposition 8 as follows "If M -> N in lambda-C--tphat{->} then, there is P ~~ N^tp such that M^tp ->>^{>=1} P in lambda-C--{->,-} for any fresh continuation variable tp." 2) State the result in lambda-C--{->,-,bot} instead of lambda-C--{->,-} and translate (tp-hat M)^tp into tp_bot(join M^tp) where tp_bot is the continuation constant associated to the elimination rule of bot. Then, we have the result in lambda-C--{->,-,bot} instead of lambda-C--{->,-} and translate (tp-hat M)^tp into tp_bot(join M^tp) where tp_bot is the continuation constant associated to the elimination rule of bot. Then, we have "If M -> N in lambda-C--tphat{->} then M^tp ->>^{>=1} N^tp in lambda-C--{->,-,bot} for any fresh continuation variable tp."