Typed Compilation Against Non-manifest Base Classes

摘要

Much recent work on proof-carrying code aims to build certifying compilers for single-inheritance object-oriented languages, such as Java or C#. Some modern object-oriented languages support compiling a derived class without complete information about its base class. This strategy—though necessary for supporting features such as mixins, traits, and first-class classes—is not well-supported by existing typed intermediate languages. We present a low-level IL 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. Languages (such as Java) that do not require such flexibility are not penalized at run time.