Type-Preserving Compilation for Large-Scale Optimizing Object-Oriented Compilers - Condit, Jeremy; Chen, Juan; Hawblitzel, Chris; Coetzee, Derrick (ACM Conference on Programming Language Design and Implementation (PLDI 08), 2008)
Type-preserving compilers translate well-typed source code, such as Java or C#, into verifiable target code, such as typed assembly language or proof-carrying code. This paper presents the implementation of type-preserving compilation in a complex, large-scale optimizing compiler. Compared to prior work, this implementation supports extensive optimizations, and it verifies a large portion of the interface between the compiler and the runtime system. This paper demonstrates the practicality of type-preserving compilation in complex optimizing compilers: the generated typed assembly language is only 2.3% slower than the base compiler's generated untyped assembly language, and the type-preserving compiler is 82.8% slower than the base compiler.