|
A Semantic Account of Type-Directed Partial Evaluation
Andrzej Filinski June 1999 |
Abstract:
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. |