In the previous chapters we have focused on the theoretical development of the language of the mixed λ-calculus and combinatory logic (Chapters 2, 3 and 4) and on the different standard and non-standard semantics of the language (Chapters 5, 6 and 7). There are two immediate application areas for this work, one is in the efficient implementation of functional languages and the other is in denotational semantics.

Optimized Code Generation

Much work in the community of functional languages has been devoted to the development of efficient implementations. This is well documented in [86] which contains a number of techniques that may be used to improve the overall performance of a ‘naive’ implementation. However, the theoretical soundness of all these techniques has not been established (although [52] goes part of the way). We believe that the main reason for this is that it is not well-understood how to structure correctness proofs even for naive code generation schemes. So although we have a firm handle on how to prove the safety of large classes of program analyses it is less clear how to formally prove the correctness of exploiting the analyses to generate ‘optimized’ code.

Before addressing the question on how to improve the code generation of Chapter 6 let us briefly review the techniques we have used. The code generation is specified as an interpretation K (in the sense of Chapter 5) and its correctness is expressed by means of Kripke-logical relations.