From System F to Typed Assembly Language

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 1998
Accession Number
ADA640223

Entities

People

  • David Walker
  • Greg Morrisett
  • Karl Crary
  • Neal Glew

Organizations

  • Cornell University

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Assembly
  • Assembly Languages
  • Computer Languages
  • Computer Programming
  • Formal Languages
  • High Level Languages
  • Information Operations
  • Instructions
  • Language
  • Programming Languages
  • Three Dimensional

Fields of Study

  • Computer science

Readers

  • Computer Vision.
  • Database Systems and Applications
  • Parallel and Distributed Computing.