Certifying compilation for standard ML in a type analysis framework

Certified code is native machine code that is annotated with an automatically checkable certificate attesting to the conformance of the program to a specified safety policy. Certified code frameworks have been built based on first-order logic (PCC) and on types (TAL). Compilers generating certified code have been built for safe subsets of C and for Java(tm).; 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 type-preserving compilers for full-scale languages maintain type information all the way to the machine-code level, and hence are not yet able to generate certified code.; 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 .