Popular 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.
12th International Conference on Compiler Construction,
Warsaw, Poland, April 2003.
Lecture Notes in
Computer Science Vol TBA
. © Springer-Verlag.