From system F to typed assembly language

We motivate the design of a typed assembly language (TAL) and present a typ e-preserving translation from System F to TAL. The typed assembly language we present is based on a conventional RISC assembly language, but its stati c type system provides support for enforcing high-level language abstractio ns, such as closures, tuples, and user-defined abstract data types. The typ e system ensures that well-typed programs cannot violate these abstractions . In addition, the typing constructs admit many low-level compiler optimiza tions. 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 contri bution is an approach to polymorphic closure conversion that is considerabl y simpler than previous work. The compiler and typed assembly language prov ide a fully automatic way to produce certified code, suitable for use in sy stems where untrusted and potentially malicious code must be checked for sa fety before execution.