PRL Seminars

Abstract

Typed Assembly Language (TAL) is a type safe version of a simple RISC assembly language augmented with memory management primitives. It could serve as a target for a type directed compiler, or as a low level version of language like JVML in a secure extensible system.

TAL was first described by Morrisett et al in POPL'98 and further refined in papers in TIC'98 and POPL'99. A group of us at Cornell have implemented a version of TAL we call TALx86 for the Intel 32 bit architecture, which supports the compilation of realistic programming languages.

In this talk, I will describe the basic concepts of TAL/TALx86 and the type system that underlies our implementation. While I will concentrate on the theory of TAL and TALx86, I will briefly touch upon how TAL is applied, the TAL system, and how the applications affect various design decisions. Familiarity with language theory is assumed.

Joint work with Karl Crary, Dan Grossman, Greg Morrisett, Richard Samuels, Frederick Smith, Dave Walker, Stephanie Weirich, and Steve Zdancewic.