Last modified: Sat Apr 9 03:11:32 2016 GMT.
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 programming 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-like source calculus into a typed lambda calculus. I prove that both languages are sound and decidable, and that the translation preserves types.
I also address many practical concerns, moving beyond the formal model to include most features of the Java language. To stage the translation, I developed lambda JVM, a novel representation of Java bytecode that is simpler to verify. I describe a prototype compiler that supports both Java and ML, sharing the same typed intermediate language, optimizers, code generator, and runtime system.