Stephanie Weirich on From System F to Typed Assembly Language

From System F to Typed Assembly Language

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 (http://www.cis.upenn.edu/~sweirich/) is a Professor of Computer and Information Science (http://www.cis.upenn.edu/) at the University of Pennsylvania.

Food and drinks will be available at 6:30PM and the talk will start at 7PM.

Directions:

Unfortunately, getting to the Greenberg Lounge can be tricky. There are two ways to get there:

1. Most dependable: Levine Hall entrance. This seems to be the entrance closest to Greenberg Lounge that won't be locked. Enter “3300 Chancellor St, Philadelphia, PA 19104” into Google Maps and enter through this entrance (https://upload.wikimedia.org/wikipedia/commons/6/68/Levine_Hall_(University_of_Pennsylvania)_-_IMG_6634.JPG). Go straight, through the door that goes to the courtyard. Walk up the steps until you reach this door (http://www.cis.upenn.edu/~dfaced/directions/cafe_03a.png). Then go straight and make a right. The lounge will then be on your right.

2. Closer but will be locked after 7PM: Skirkanich Entrance on S 33rd St. This entrance (https://c2.staticflickr.com/4/3411/3278952033_1828f2ce1d.jpg) will be easier to find. I'll be there to let people in until 7PM when the talk will start.
   If anyone has trouble getting to Greenberg Lounge, please post on the meetup page. I'll be checking it frequently.

Food and drinks sponsored by Chariot Solutions:

Chariot Solutions is passionate about technology. We work with a wide variety of technologies, and solve an even wider variety of problems. We value learning, working with the best people and delivering great products for our customers. And we are hiring. chariotsolutions.com (http://chariotsolutions.com/)