From system F to typed assembly language

Greg Morrisett, David Walker, Karl Crary, Neal Glew

Research output: Contribution to journalConference articlepeer-review

200 Scopus citations

Abstract

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 languageEnglish (US)
Pages (from-to)85-97
Number of pages13
JournalConference Record of the Annual ACM Symposium on Principles of Programming Languages
DOIs
StatePublished - Jan 1 1998
Externally publishedYes
EventProceedings of the 1998 25th ACM SIGPLAN SIGACT Symposium on Principles of Programming Languages - San Diego, CA, USA
Duration: Jan 19 1998Jan 21 1998

All Science Journal Classification (ASJC) codes

  • Software

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

Cite this