From System F to Typed Assembly Language
Abstract
We motivate the design of a {\em typed assembly language} (TAL) and present
a type-preserving translation from System F to TAL. The typed assembly
language 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 user-defined
abstract data types. The type system ensures that well-typed programs
cannot violate these abstractions. In addition, the typing constructs
admit many low-level compiler optimizations. 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 certified code, suitable for
use in systems where untrusted and potentially malicious code must be
checked for safety before execution.
(postscript)