Method Inlining, Dynamic Class Loading, and Type Soundness

Abstract

Method inlining is an optimisation that can be invalidated by later class loading. In this paper a framework for reasoning about method inlining, dynamic class loading, and type soundness is discussed. The example language has both a nonoptimising and an optimising semantics. The two semantics are equivalent and both have a type soundness property, proving the correctness and type safety of the optimisation. The framework can form the basis of virtual machines that represent optimised code in a typed low-level language.

Cite as:

Neal Glew, Jens Palsberg, “Method Inlining, Dynamic Class Loading, and Type Soundness”, Journal of Object Technology, Volume 4, no. 8 (October 2005), pp. 33-53, doi:10.5381/jot.2005.4.8.a2.