By Atsushi Igarashi and Benjamin C. Pierce. Information and Computation, 177(1):56-89, August 2002.
Earlier versions appeared in Proceedings of the Fourteenth European Conference on Object-Oriented Programming (ECOOP2000), Springer LNCS 1850, pages 129-153, Cannes, France, June 2000 and in Informal Proceedings of the Seventh International Workshop on Foundations of Object-Oriented Languages (FOOL 7), Boston, MA, January 2000.
Inner classes in object-oriented languages play a role similar to nested function definitions in functional languages, allowing an object to export other objects with direct access to its own methods and instance variables. However, the similarity is deceptive: a close look at inner classes reveals significant subtleties arising from their interactions with inheritance.
The goal of this work is a precise understanding of the essential features of inner classes; our object of study is a fragment of Java with inner classes and inheritance (and almost nothing else). We begin by giving a direct reduction semantics for this language. We then give an alternative semantics by translation into a yet smaller language with only top-level classes, closely following Java's Inner Classes Specification. We prove that the two semantics coincide, in the sense that translation commutes with reduction, and that both are type-safe.