The TAL Project

Gregg Morrisett
Department of Computer Science
Cornell University
jgm@cs.cornell.edu

The TAL Manifesto

Statically typed intermediate languages are effective tools for staging the compilation of high-level languages. Types express invariants that help programmers understand their programs and strongly typed languages prevent many common programming errors. Compiler writers can use these properties to debug sophisticated program transformations such as closure conversion and optimizations such as datatype specialization. Moreover, many of these optimizations are not only type-preserving but actually type-directed; the type of an object guides its translation.

The goal of the TAL project is to extend the paradigm of type-directed compilation to its limit. We compile a high-level language (KML) which includes higher-order polymorphic functions, datatypes, modules, functors, objects, and subtyping through a series of typed intermediate languages and finally into a Typed Assembly Language (TAL). Unlike any other compiler, we not only use typed intermediate languages but also typed target languages.

TALC, our compiler, generates code for the Intel 386 family of assembly languages which is then verified by our type checker before being assembled by the MASM assembler. The few typing annotations on the code are comments which are erased during the assembler's translation. The assembly language type system is powerful enough to express high-level abstractions such as closures and abstract datatypes and yet flexible enough to permit traditional low-level optimizations such as loop invariant removal, strength reduction, and redundant move elimination.  Furthermore, just as the more familiar typed source and intermediate languages catch programmer errors, so does our typed assembly language. It helps to ensure that complicated backend transformations such as the optimizations above as well as register allocation and more general instruction selection and scheduling are performed correctly.

The type soundness of our assembly code implies many important security properties such as memory safety. As a result, our assembly code is a form of proof-carrying code. TAL applets, like Java applets, may be downloaded from untrusted sources on the internet, verified, and executed safely without fear they will corrupt the host machine.   Furthermore, because TAL is assembly language, there is no interpretation overhead and no just-in-time compiler to run or trust.

The present TAL effort has many applications in the security and compilation domains. Future work involves compiling more expressive typed languages into the language of real machines. We seek to reveal the connections between the typed lambda calculi which give semantics to many modern languages and the Von Neumann machines which implement them.

TAL Papers

TALC Implementation

We are currently implementing a compiler for the KML programming language which generates TAL code. Futurereleases of the compiler will be available from this site. For now, take a look at the following example factorial program and the corresponding TAL code that our compiler generates.

TAL Project Members

Related Projects

This page is maintained by walker@cs.cornell.edu, last updated on 12 February 1998.