From system F to typed assembly language

Greg Morrisett, David Walker, Karl Crary, Neal Glew

Research output: Contribution to journalArticle

351 Scopus citations

Abstract

We motivate the design of a 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.

Original languageEnglish (US)
Pages (from-to)527-568
Number of pages42
JournalACM Transactions on Programming Languages and Systems
Volume21
Issue number3
DOIs
StatePublished - May 1999

All Science Journal Classification (ASJC) codes

  • Software

Keywords

  • Certified code
  • Closure conversion
  • Secure extensible systems
  • Type-directed compilation
  • Typed assembly language
  • Typed intermediate languages

Fingerprint Dive into the research topics of 'From system F to typed assembly language'. Together they form a unique fingerprint.

  • Cite this