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
Wean 8220