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.
|Original language||English (US)|
|Number of pages||13|
|Journal||Conference Record of the Annual ACM Symposium on Principles of Programming Languages|
|State||Published - Jan 1 1998|
|Event||Proceedings of the 1998 25th ACM SIGPLAN SIGACT Symposium on Principles of Programming Languages - San Diego, CA, USA|
Duration: Jan 19 1998 → Jan 21 1998
All Science Journal Classification (ASJC) codes