The Correctness of an Optimized Code Generation

Abstract

For a functional programming language with a lazy standard semantics, we define a strictness analysis by means of abstract interpretation. Using the information from the strictness analysis we are able to define a code generation which avoids delaying the evaluation of the argument to an application, provided that the corresponding function is strict.

To show the correctness of the code generation, we adopt the framework of logical relations and define a layer of predicates which finally will ensure that the code generation is correct with respect to the standard semantics.