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
|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.
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.