Home TAL Overview Papers Software Members Related Projects


The current implementation of Typed Assembly Language, TALx86, is based on Intel's IA32 architecture. This implementation extends the theoretical calculi described in our papers and provides support for sums, arrays, references, recursive types, subtyping, type tagging, and modules, among other features. Our distributions contain our Objective Caml source code and executables for the following:

TAL tools including a type-checker for the assembly language.
Popcorn: A prototype compiler for a safe C-like language.
SCHEME--: A prototype compiler for a subset of the scheme language (written in Popcorn).

The software is currently pre-alpha, contains little documentation, and comes with absolutely no warranty. Use at your own risk!  All code is copyright by Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Fred Smith, David Walker, Stephanie Weirich, and Steve Zdancewic. July, August, September 1998, January, and July 1999. All rights reserved.

Release 3.0 (WinZip file)
Release 2.0 (WinZip file)
Release 1.7 (WinZip file)
Release 1.6 (WinZip file)
Release 1.5 (WinZip file)
Release 1.4 (WinZip file)
Release 1.3 was skipped.
Release 1.2 (WinZip file)
Release 1.1 (WinZip file)
Release 1.0 (WinZip file)
popcorna.jpg (86079 bytes)

Just for fun, we entered the ICFP'99 programming contest using TAL as our programming language.  Astonishingly, we were the only group to submit provably safe code to the contest organizers.  Our hats off to them and their courage for running so many untrusted applications.  Here is our entry.


Linear TAL: A linearly typed variant of TAL that manages its own memory through linear alias tracking.

Source available here.