From System F to Typed Assembly Language (Extended Version)
| dc.contributor.author | Morrisett, Greg | en_US |
| dc.contributor.author | Walker, David | en_US |
| dc.contributor.author | Crary, Karl | en_US |
| dc.contributor.author | Glew, Neal | en_US |
| dc.date.accessioned | 2007-04-23T18:10:59Z | |
| dc.date.available | 2007-04-23T18:10:59Z | |
| dc.date.issued | 1997-11 | en_US |
| dc.description.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. | en_US |
| dc.format.extent | 494144 bytes | |
| dc.format.extent | 470192 bytes | |
| dc.format.mimetype | application/pdf | |
| dc.format.mimetype | application/postscript | |
| dc.identifier.citation | http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR97-1651 | en_US |
| dc.identifier.uri | https://hdl.handle.net/1813/7305 | |
| dc.language.iso | en_US | en_US |
| dc.publisher | Cornell University | en_US |
| dc.subject | computer science | en_US |
| dc.subject | technical report | en_US |
| dc.title | From System F to Typed Assembly Language (Extended Version) | en_US |
| dc.type | technical report | en_US |