A Semantic Account of Type-Directed Partial Evaluation | Zendy

Andrzej Filinski | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

A 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.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research