We formally characterize partial evaluation of functional pro- grams 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 simplic- ity, 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.
CITATION STYLE
Filinski, A. (1999). A semantic account of type-directed partial evaluation. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1702, pp. 378–395). Springer Verlag. https://doi.org/10.1007/10704567_23
Mendeley helps you to discover research relevant for your work.