Abstract: Type-preserving compilers translate well-typed source code into verifiable target code, so that we do not have to trust the compilers.  This talk explains our experience with type-preserving compilation in large-scale object-oriented compilers.  Our type systems are simpler than existing class and object encodings, yet expressive enough to describe standard implementation techniques for object-oriented primitives.  We implemented the type systems in an optimizing compiler with 200,000 lines of code, an order of magnitude larger than existing systems.  The generated target code is only 2.3% slower than the base compiler's generated untyped code, and the type-preserving compiler is 42% slower than the base compiler.

Juan Chen received her PhD from Princeton in 2004.  She is a researcher in the Advanced Compiler Technology group at Microsoft Research.