Precision in Practice: A Type-Preserving Java Compiler
Last modified: Wed Jan 29 14:51:26 2003 GMT.
AbstractPopular mobile code architectures (Java and .NET) include verifiers to check for memory safety and other security properties. Since their formats are relatively high level, supporting a wide range of source language features is awkward. Further compilation and optimization, necessary for efficiency, must be trusted. We describe the design and implementation of a fully type-preserving compiler for Java and SML. Its strongly-typed intermediate language, provides a low-level abstract machine model and a type system general enough to prove the safety of a variety of implementation techniques. We show that precise type preservation is within reach for real-world Java systems.
Published12th International Conference on Compiler Construction, Warsaw, Poland, April 2003. Lecture Notes in Computer Science Vol TBA. © Springer-Verlag.
Copyright © 1996-2021 The FLINT Group
<flint at cs dot yale dot edu>
Yale University Department of Computer Science