A Semantic Account of Type-Directed Partial Evaluation
We formally characterize partial evaluation of functional programs as a
normalization problem in an equational theory, and derive a type-based
normalization-by-evaluation algorithm for computing normal forms in this
setting. We then establish the correctness of this algorithm using a
semantic argument based on Kripke logical relations. For simplicity,
the results are stated for a non-strict, purely functional language; but
the methods are directly applicable to stating and proving correctness
of type-directed partial evaluation in ML-like languages as well.
Full document:
DVI or
PostScript.