Open AccessA Semantic Account of Type-Directed Partial Evaluation
Author(s) -
Andrzej Filinski
Publication year - 1999
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v6i17.20074
Subject(s) - correctness , normalization (sociology) , partial evaluation , computer science , logical consequence , functional programming , type (biology) , type theory , programming language , algorithm , theoretical computer science , mathematics , artificial intelligence , ecology , sociology , anthropology , biology
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.