Typed Assembly Language for Object-Oriented Compilers

We study techniques to guarantee safety properties of native code through typed intermediate languages and Typed Assembly Languages (TAL). TAL requires the compiler generate native code with type annotations and a verifier check the annotated native code. This way, we do not have to trust the compiler. We focus on large-scale optimizing object-oriented compilers.