A Semantic Account of Type-Directed Partial Evaluation

  • Andrzej Filinski


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.
How to Cite
Filinski, A. (1999). A Semantic Account of Type-Directed Partial Evaluation. BRICS Report Series, 6(17). https://doi.org/10.7146/brics.v6i17.20074