[TYPES] Lambda calculus with callcc and Moggi's monadic metalanguage

[emakarov]

I am studying simply-typed call-by-value (CBV) lambda calculus with 
Felleisen's control operator C, or with Scheme's call/cc. For my goal 
(removing useless subterms of singleton type) I need beta reductions which 
are more general than CBV ones, namely, which allow a function's argument to 
be any "pure" term and not necessarily a value. Here "pure" means that the 
term does not invoke control operators, i.e., does not cause side effects.

I think that it would be convenient to translate this lambda calculus into 
Moggi's monadic metalanguage (MML) which explicitly separates terms with 
side effects from pure terms. Terms with side effects have type (M sigma) 
where M is a new type constructor, and they have to be evaluated using a 
special construct do x <- t1; t2 (computational reductions). Pure terms, on 
the other hand, admit arbitrary beta reductions.

However, I believe that just defining the translation does not solve 
anything. One has to actually prove that beta reductions on pure term do not 
change the program's answer. So one has to prove something like bisimulation 
between computational and beta reductions.

I am wondering if somebody has defined this translation from lambda calculus 
with control operators into MML and proved the corresponding properties. 
More precisely, I'd like to know if

(1) there is a translation which inserts the least number of M's (for 
example, it should *not* change every function type sigma1 -> sigma2 into 
sigma1 -> M sigma2). Ideally, only terms with side effects should have type 
starting with M.

(2) it is proved that arbitrary beta reductions do not change the program's 
answer.

Thank you for your help.

Yevgeniy