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.

Full Text:


DOI: http://dx.doi.org/10.7146/brics.v6i17.20074
This website uses cookies to allow us to see how the site is used. The cookies cannot identify you or any content at your own computer.

ISSN: 0909-0878 

Hosted by the Royal Danish Library and Aarhus University Library