Abstract A Type-Preserving Compiler Infrastructure

Many kinds of networked devices receive and execute new programs from various sources. Since we may not fully trust the producers of these programs, we must take measures to ensure that such code does notmisbehave. Currently deployedmobile code formats can be checked for memory safety and other security properties, but they are relatively high-level. A type-preserving compiler generates lower-level, more optimized code that is still verifiable. This increases assurance by reducing the trusted computing base; we need not trust the compiler anymore. Moreover, lower-level representations naturally support a wider variety of source languages. Previous research on type-preserving compilation focused on functional languages or safe subsets of C. How to adapt this technology to more widely-used object-oriented languages was unknown. This dissertation explores techniques that enable a single strongly-typed intermediate language to certify programs in two very different pro-gramming languages: Java and ML. The major contribution is an efficient new encoding of object-oriented constructs into a typed intermediate language. I give a complete formal translation of a Java-lik