| Typed Assembly Language (TAL) is a formal language for an idealised machine augmented with type annotations, typing rules, and a memory allocation primitive. TAL's type system is sound; that is, well typed TAL programs do not commit run-time type errors during execution. This guarantee can be used to debug type-directed compilers and to build more general security properties in an extensible system. This dissertation presents a basic version of TAL and extensions to support the compilation of modules and object-oriented languages. First, it describes a modular version of TAL that consists of typed object files, linking operations, and link compatibility conditions. Together these features provide for type-sound separate compilation and substantially extend previous work on linking. Second, it shows how to use a new formulation of self quantifiers to compile an efficient implementation of a single-inheritance class-based object-oriented language into TAL. Third, it presents a new type constructor called a tag type, and shows how to use them to compile downcasting and exceptions into TAL. |
