Rob O'Callahan
A Simple, Comprehensive Type System for Java Bytecode Subroutines
A type system with proven soundness is a prerequisite for the safe and efficient
execution of Java bytecode programs. So far, efforts to construct such a type
system have followed a "forward dataflow" approach, in the spirit of the original
Java Virtual Machine bytecode verifier. We present an alternative type system,
based on conventional ideas of type constraints, polymorphic recursion and
continuations. We compare it to Stata and Abadi's JVML-0 type system for bytecode
subroutines, and demonstrate that our system is simpler and able to type strictly
more programs, including code that could be produced by Java compilers and cannot
be typed in JVML-0. Examination of real Java programs shows that such code is rare
but does occur. We explain some of the apparently arbitrary constraints imposed by
previous approaches by showing that they are consequences of our simpler type
rules, or actually unnecessary.
October 30, 1998
3:30pm
Wean 8220