A Semantic Account of Type-Directed Partial Evaluation

Andrzej Filinski

June 1999


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

Available as PostScript, PDF, DVI.


Last modified: 2003-06-08 by webmaster.