From System F to Typed Assembly Language
We motivate the design of a typed assembly language (TAL) by presenting a type-preserving translation from System F to our TAL. The TAL we present is based on a conventional RISC assembly language, but its static type system ensures that well-typed programs cannot "go wrong." Furthermore, the type system presented here is sufficiently powerful that we can compile polymorphic, recursive, and higher-order functions; abstract data types; objects; and a variety of other language mechanisms to highly-optimized but type-correct TAL code.
We sketch such a compiler as a sequence of type-directed translations.
Inspired by SML/NJ, the compiler uses CPS and closure conversion
phases, but unlike SML/NJ, maintains types throughout compilation. In
addition, we present 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