Authors
Christopher League
Zhong Shao
Valery Trifonov
Abstract
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.
Published
12th International Conference on Compiler Construction,
Warsaw, Poland, April 2003.
Lecture Notes in
Computer Science Vol TBA. © Springer-Verlag.