Abstract
The second lecture focused on compilation: the automatic translation of a high-level programming language into machine-executable code. As programming languages have evolved, numerous compilation and program optimization algorithms have been developed, transforming code to increase performance. All these transformations are not without risk : an error in the compiler can cause it to produce false executable code from a correct source program ; this is known as mis-compilation.
To avoid any mis-compilation, it is sufficient to formally verify the compiler itself, by demonstrating that the semantics of the compiled code are faithful to the semantics of the source program. This is an old field of research, with the first work by McCarthy and Painter in 1967 and the first mechanized verification by Milner and Weyrauch in 1972, but it is still very active today.
The lecture explored this verification approach on a simple compiler (without optimizations) for the IMP language, producing code for a virtual machine using a stack. A first demonstration, using the natural semantics of the IMP language, shows without too much trouble the preservation of the semantics of terminating IMP programs.
To extend this result to all IMP programs, including those that diverge, we studied the technique of simulation diagrams between two semantics with reductions. However, the reduction semantics of IMPs studied in the first lecture do not lend themselves easily to the construction of such a diagram for our compiler. We have therefore introduced another transition semantics for IMP, based on continuations and reductions under context, partly inspired by focusing in demonstration theory. This semantics allows the construction of a simulation diagram that shows the semantic preservation of our compiler.
