A Computational Formalization for Partial Evaluation (Extended Version) - Hatcliff, John; Danvy, Olivier (BRICS Report Series, 1996)
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, and 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.