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