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:

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.