A Simple, Comprehensive Type System for Java Bytecode Subroutines

Author: Robert O'Callahan

Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on the Principles of Programming Languages. San Antonio, Texas, January 20-22, 1999.

Download the Postscript or PDF

Abstract

A type system with proven soundness is a prerequisite fo rthe 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.

Keywords: Java, bytecode, types, subroutines, continuations, polymorphic recursion

Brought to you by Composable Software Systems Research Group in the School of Computer Science at Carnegie Mellon University.

[Last modified 26-Aug-1999.
Mail suggestions to the Maintainer.]