Provably Correct Code Generation: A Case Study

Provably correct compilation is an important aspect in development of high assurance software systems. In this paper we present an approach to provably correct compilation based on Horn logical semantics of programming languages and partial evaluation. We also show that continuation semantics can be expressed in the Horn logical framework, and introduce Definite Clause Semantics. We illustrate our approach by developing the semantics for the SCR specification language, and using it to (automatically) generate target code in a provably correct manner.