TY - GEN

T1 - Java bytecode as a typed term calculus

AU - Higuchi, Tomoyuki

AU - Ohori, Atsushi

PY - 2002/12/1

Y1 - 2002/12/1

N2 - We propose a type system for the Java bytecode language, prove the type soundness, and develop a type inference algorithm. In contrast to the existing proposals, our type system yields a typed term calculus similar to type systems of lambda calculi. This enables us to transfer existing techniques and results of type theory to a JVM-style bytecode language. We show that ML-style let polymorphism and recursive types can be used to type JVM subroutines, and that there is an ML-style type inference algorithm. The type inference algorithm has been implemented. The ability to verify type soundness is a simple corollary of the existence of type inference algorithm. Moreover, our type theoretical approach opens up various type safe extensions including higher-order methods, flexible polymorphic typing through polymorphic type inference, and type-preserving compilation.

AB - We propose a type system for the Java bytecode language, prove the type soundness, and develop a type inference algorithm. In contrast to the existing proposals, our type system yields a typed term calculus similar to type systems of lambda calculi. This enables us to transfer existing techniques and results of type theory to a JVM-style bytecode language. We show that ML-style let polymorphism and recursive types can be used to type JVM subroutines, and that there is an ML-style type inference algorithm. The type inference algorithm has been implemented. The ability to verify type soundness is a simple corollary of the existence of type inference algorithm. Moreover, our type theoretical approach opens up various type safe extensions including higher-order methods, flexible polymorphic typing through polymorphic type inference, and type-preserving compilation.

KW - Bytecode verifier

KW - Java bytecode

KW - Type inference

KW - Type system

UR - http://www.scopus.com/inward/record.url?scp=0036992547&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0036992547&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:0036992547

SN - 1581135289

T3 - Proceedings of the ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP'02)

SP - 201

EP - 211

BT - Proceedings of the ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP'02)

T2 - Proceedings of the Fourth ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP'02)

Y2 - 6 October 2002 through 8 October 2002

ER -