Stephanie Weirich on From System F to Typed Assembly Language
Channel: Papers We Love Philadelphia
Date: 07/10/2015

by Greg Morrisett, David Walker, Karl Crary and Neal Glew

Abstract: We motivate the design of a typed assembly language (TAL) and present a type-preserving translation from System F to TAL. The typed assembly language 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 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.

Even though it is a technical paper, the lecture will not assume any background in programming language research or type systems from the audience. 

Paper: https://www.cs.princeton.edu/~dpw/papers/tal-toplas.pdf

Stephanie Weirich is a Professor of Computer and Information Science at the University of Pennsylvania.

http://www.cis.upenn.edu/~sweirich/

Food sponsored by http://chariotsolutions.com