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.
Specifically, we prove that the binding-time improvements given by
‘continuation-based
specialization’ can be expressed in the metalanguage via monadic
laws.
Extended Call-by-Push-Value: Reasoning About Effectful Programs and Evaluation Order