The goal of semantics-directed compilation is to develop an efficient implementation from a formal definition in such a way that correctness can be verified. Denotational semantics is a formally-based notation which has been used to describe compilers; however, most of the work done thus far has dealt with code generation. Recent results show how denotational semantics can be used to model other phases of compilation besides code generation. As background, a specification and proof of correctness of an optimizing compiler is given for a block-structured language with loops. Semantics-preserving transformations are used to convert a continuation semantics into a formal description of a compiler which does some simple optimizations based on type analysis. Both the flow analysis and code generation are proved correct with respect to the source language semantics. This project will extend this methodology to derive provably correct specifications of more realistic compilers.
