A Computational Formalization for Partial Evaluation (Extended Version)

John Hatcliff
Olivier Danvy

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

Available as PostScript, PDF, DVI.


Last modified: 2003-06-08 by webmaster.