Sciweavers

POPL
1998
ACM

From System F to Typed Assembly Language

13 years 7 months ago
From System F to Typed Assembly Language
abstractions, such as closures, tuples, and user-defined abstract data types. The type system ensures that well-typed programs cannot violate these abstractions. In addition, the typing constructs admit many low-level compiler optimizations. 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 certified code, suitable for use in systems where untrusted and potentially malicious code must be checked for safety before execution. Categories and Subject Descriptors: D.2.11 [Software Engineering]: Software Architectures— Languages; D.3.1 [Programming Languages]: Formal Definitions and Theory—Semantics, Syntax; D.3.2 [Programming Language...
J. Gregory Morrisett, David Walker, Karl Crary, Ne
Added 05 Aug 2010
Updated 05 Aug 2010
Type Conference
Year 1998
Where POPL
Authors J. Gregory Morrisett, David Walker, Karl Crary, Neal Glew
Comments (0)