Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 A Semantic Account of Type-Directed Partial Evaluation (abstract)
A Semantic Account of Type-Directed Partial Evaluation
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.