From system F to typed assembly language

We motivate the design of typed assembly language (TAL) and present a type-preserving ttranslation from Systemn F to TAL. The typed assembly language we pressent is based on a conventional RISC assembly language, but its static type sytem provides support for enforcing high-level language abstratcti...

Full description

Saved in:
Bibliographic Details
Published in:ACM transactions on programming languages and systems 1999-05, Vol.21 (3), p.527-568
Main Authors: Morrisett, Greg, Walker, David, Crary, Karl, Glew, Neal
Format: Article
Language:English
Subjects:
Assembly languages
Compilers
Context specific languages
Formal language definitions
General programming languages
Language types
Macro languages
Operational semantics
Program constructs
Program semantics
Semantics
Semantics and reasoning
Software and its engineering
Software architectures
Software notations and tools
Software organization and properties
Software system structures
Syntax
System description languages
Theory of computation
Type structures
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We motivate the design of typed assembly language (TAL) and present a type-preserving ttranslation from Systemn F to TAL. The typed assembly language we pressent is based on a conventional RISC assembly language, but its static type sytem provides support for enforcing high-level language abstratctions, such as closures, tuples, and user-defined abstract data types. The type system ensures that well-typed programs cannot violatet these abstractionsl In addition, the typing constructs admit many low-level compiler optimiztaions. 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 lanugage provide a fully automatic way to produce certified code, suitable for use in systems where unstrusted and potentially malicious code must be checked for safety before execution.
ISSN:0164-0925
1558-4593
DOI:10.1145/319301.319345