We formalize a partial evaluator for Eugenio Moggi's computational metalanguage. This formalization gives an evaluation-order independent view of binding-time analysis and program specialization, including a proper treatment of call unfolding. It also enables us to express the essence of `control-based binding-time improvements' for let expressions.
Specically, we prove that the binding-time improvements given by `continuation-based specialization' can be expressed in the metalanguage via monadic laws.