Abstract
We present a methodology for realistic compiler development in an existing formal methods framework. Program transformations and analyses are implemented as term rewrites and inference rules, and automated proof search techniques are used to drive the compilation process. This approach allows the programmer to implement the compiler succinctly, declaratively, and modularly. We explain how our methodology separates trusted code, which can potentially corrupt compilation, from untrusted code, which cannot. We present a case study in which we have used these techniques to implement a compiler for a small ML-like programming language that produces x86 assembly code as output. We give a detailed overview of several stages of the compiler, including type inference, type checking, type erasure, CPS conversion, and closure conversion. We also describe the process of extending the minimal core compiler to include features such as integers, Booleans, operators, tuples, and recursive functions.
|
