From system F to Typed Assembly Language
MetadataShow full item record
CitationMorrisett, Greg, David Walker, Karl Crary, and Neal Glew. From system f to typed assembly language. Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 85-97, New York, NY, USA, 1998. ACM.
AbstractWe 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.
Citable link to this pagehttp://nrs.harvard.edu/urn-3:HUL.InstRepos:2797451
- FAS Scholarly Articles