We motivate the design of a statically typed assembly language (TAL) and
present a type-preserving translation from System F to TAL. The TAL we present is based on
a conventional RISC assembly language, but its static type system provides support for
enforcing high-level language abstractions, such as closures, tuples, and objects, as well
as user-defined abstract data types. The type system ensures that well-typed programs
cannot violate these abstractions. In addition, the typing constructs place almost no
restrictions on low-level optimizations such as register allocation, instruction
selection, or instruction scheduling.
Our translation to TAL is specified as a sequence of type-preserving transformations,
including CPS and closure conversion phases; type-correct source programs are mapped to
type-correct assembly language. A key contribution is an approach to polymorphic closure
conversion that is considerably simpler than previous work. The compiler and typed
assembly language provide a fully automatic way to produce proof carrying code,
suitable for use in systems where untrusted and potentially malicious code must be checked
for safety before execution.