From system F to Typed Assembly Language
| Title: | From system F to Typed Assembly Language |
| Author: |
Crary, Karl; Morrisett, John Gregory; Walker, David; Glew, Neal
Note: Order does not necessarily reflect citation order of authors. |
| Citation: | Morrisett, 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. |
| Full Text & Related Files: |
Morrisett_FtoTypedAssembly.pdf (196.3Kb; PDF) 
|
| 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. |
| Published Version: | http://doi.acm.org/10.1145/268946.268954 |
| Terms of Use: | This article is made available under the terms and conditions applicable to Other Posted Material, as set forth at http://nrs.harvard.edu/urn-3:HUL.InstRepos:dash.current.terms-of-use#LAA |
| Citable link to this page: | http://nrs.harvard.edu/urn-3:HUL.InstRepos:2797451 |
This item appears in the following Collection(s)
-
FAS Scholarly Articles [5171]
Peer reviewed scholarly articles from the Faculty of Arts and Sciences of Harvard University
Contact administrator regarding this item (to report mistakes or request changes)
