Typed compilation against non-manifest base classes

Abstract. Much recent work on proof-carrying code aims to build certifying compilers for single-inheritance object-oriented languages, such as Java or C#. Some advanced object-oriented languages (such as Loom, Moby, and OCaml) support compiling a derived class without complete information about its base class. This strategy is necessary for supporting features such as mixins and firstclass classes. Fisher, Reppy, and Riecke designed Links, an untyped intermediate representation with abstractions suitable for compiling and optimizing a wide variety of object-oriented languages. Unfortunately, the key abstractions of Links are not typable in existing typed intermediate languages. We present a low-level intermediate language inspired by Links, but with a type system based on the Calculus of Inductive Constructions. It is an appropriate target for efficient, type-preserving compilation of various forms of inheritance, even when the base class is unknown at compile time. Moreover, languages (such as Java) that do not require such flexibility are not penalized for it at run time. 1