Open AccessThe Correctness of an Optimized Code Generation
Author(s) -
Torben Poort Lange
Publication year - 1992
Publication title -
daimi pb
Language(s) - English
Resource type - Journals
eISSN - 2245-9316
pISSN - 0105-8517
DOI - 10.7146/dpb.v21i427.6741
Subject(s) - correctness , programming language , computer science , abstract interpretation , semantics (computer science) , code generation , code (set theory) , functional programming , program analysis , theoretical computer science , algorithm , key (lock) , computer security , set (abstract data type)
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.