Described herein are typed intermediate representations of object-oriented
source code that preserve notions of class names, as well as add
structure-based information related to classes in the source code. Types
in the intermediate representation are divided into corresponding class
name-based types and associated structure-based record types. The
structure-based record type comprises a layout of objects that are
instances of the corresponding class name-based types, where the object
comprises one or more data fields and one or more virtual method members.
Dynamic types can be abstracted in the form of existential types with
sub-classing bounded quantifications. This makes type checking decidable.
Existential types bind type variables with sub-classing bounds to
represent dynamic types of objects. The layout of those objects can be
approximated by structure-based record types. The types of virtual
methods in the approximation record types include type variables that
represent the dynamic types of those objects to guarantee safety.