Computer Science Department
School of Computer Science, Carnegie Mellon University
Certifying Compilation for Standard ML in a Type Analysis Framework
Leaf Eames Petersen
Type-preserving compilers such as the TILT/ML compiler implement compilation as transformations on typed internal languages. Types are used by the compiler for internal verification, and for optimization purposes. Type analysis can be used to implement optimizations such as non-uniform data representation and tag-free garbage collection. However, none of the existing such compilers for full-scale languages maintain type information all the way to the machine-code level.
In this thesis, I demonstrate that certified compilation is possible in a type analysis framework by extending the TILT/ML compiler to generate certified code in the form of typed assembly language without compromising the existing optimizations of the compiler. This work demonstrates that a compiler can use types to generate certified binaries for a full modern language even in the presence of aggressive type-analysis based optimization.