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 derivea type-based normalization-by-evaluation algorithm for computingnormal forms in this setting. We then establish the correctness of this algorithm using a semantic argument based on Kripkelogical relations. For simplicity, the results are stated for a non-strict, purely functional language; but the methods are directlyapplicable to stating and proving correctness of type-directed partialevaluation in ML-like languages as well