Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Type-Preserving Compilation for Large-Scale Optimizing Object-Oriented Compilers

Juan Chen, Chris Hawblitzel, Frances Perry, Mike Emmi, Jeremy Condit, Derrick Coetzee, and Polyvios Pratikakis

Abstract

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.

Details

Publication typeInproceedings
Published inACM Conference on Programming Language Design and Implementation (PLDI 08)
PublisherAssociation for Computing Machinery, Inc.
> Publications > Type-Preserving Compilation for Large-Scale Optimizing Object-Oriented Compilers