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 unt..