Java bytecode as a typed term calculus

Tomoyuki Higuchi, Atsushi Ohori

Research output: Chapter in Book/Report/Conference proceedingConference contribution

9 Citations (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationProceedings of the ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP'02)
Pages201-211
Number of pages11
Publication statusPublished - 2002 Dec 1
EventProceedings of the Fourth ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP'02) - Pittsburg, PA, United States
Duration: 2002 Oct 62002 Oct 8

Publication series

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

Other

OtherProceedings of the Fourth ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP'02)
CountryUnited States
CityPittsburg, PA
Period02/10/602/10/8

Keywords

  • Bytecode verifier
  • Java bytecode
  • Type inference
  • Type system

ASJC Scopus subject areas

  • Engineering(all)

Fingerprint Dive into the research topics of 'Java bytecode as a typed term calculus'. Together they form a unique fingerprint.

Cite this