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