Precision in Practice: A Type-Preserving Java Compiler

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 ML. ngly-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.

• Type: Conference
• Year: 2003
• Where: CC
• Authors: Christopher League, Zhong Shao, Valery Trifonov
• Keywords: CC 2003, Mobile Code Architectures, Precise Type Preservation, Programming Languages, Real-world Java Systems