Leaf Eames Petersen

Certifying Compilation for Standard ML in a Type Analysis Framework Degree Type: Ph.D. in Computer Science
Advisor(s): Robert Harper, Karl Crary
Graduated: May 2005

Abstract:

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 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.

Thesis Committee:
Robert Harper (Chair)
Karl Crary
Peter Lee
Greg Morrisett (Harvard University)

Jeannette Wing, Head, Computer Science Department
Randy Bryant, Dean, School of Computer Science

Keywords:
Types, Compilers, Standard ML, Typed Assembly Language, Certifying Compilation, Typed Register Allocation, Type Analysis