Try ATS on-line
The ATS Programming Language
Unleashing the Potentials of Types and Templates!


ATS/Proto, written in OCaml, is the first released implementation of ATS, consisting of a typechecker (for linear types and dependent types), a closure-based interpreter and a compiler (to C). And the language implemented by ATS/Proto is often referred to as ATS0, which amounts to something like a pre-first edition of ATS. In this implementation, the standard boxed data representation is chosen to implement parametric polymorphism. There is direct support in ATS/Proto for object-oriented programming (OOP), which is no longer available in later implementations of ATS. Also, there is support in ATS/Proto for typed meta-programming (MP), that is, constructing programs that can generate well-typed programs, which is also abandoned in later implementations. As of now, ATS/Proto is no longer actively maintained and its main purpose is to serve as a historic reference.


ATS/Geizella, written in OCaml, is a previously released implementation of ATS1 (the 1st edition of ATS). In this implementation, the native unboxed data representation (as is in C) is adopted, making ATS/Geizella particularly well-suited for direct interaction with C (that incurs no run-time overhead). As for parametric polymorphism, it is supported in ATS/Geizella through the use of templates. ATS/Geizella is now largely out of active use as ATS/Anairiats, another implementation of ATS1 that is also nearly entirely written in ATS1, can be self-bootstrapped successfully. At this point, ATS/Geizella primarily serves as the backup for ATS/Anairiats in case it is needed for building ATS/Postiats, which implements ATS2 (the 2nd edition of ATS).


ATS/Anairiats is the second previously released implementation of ATS1. It is nearly entirely written in ATS1 itself, consisting of 100K+ lines of source code. When compared to ATS/Geizella, the first implementation of ATS1 (written in OCaml), ATS/Anairiats is significantly more efficient, and it issues in general more informative messages for identifying program errors. ATS/Anairiats is currently being actively used for the purpose of developing ATS/Postiats, which implements ATS2 (the 2nd edition of ATS).


ATS/Postiats is the currently released implementation of ATS2 (the 2nd edition of ATS). ATS/Postiats is nearly entirely implemented in ATS1, consisting of 180K+ lines of source code. Its major improvement over ATS1 lies in a highly versatile template system that aims at maximally facilitating code reuse. Note that ATS/Postiats is in general unable to compile code written in ATS1. However, turning ATS1 code into legal ATS2 code is largely a straightforward process due to the great syntactic similarity between ATS1 and ATS2.


ATS/Xanadu is the first implementation of ATS3 (the 3rd edition of ATS) that is currently being actively devoloped in ATS/Postiats. ATS/Xanadu aspires to turning ATS from a programming language for research into one that is of production strength for large-scale industrial software development. Please keep tuned.

A little history of ATS

(following the implementation trail)

Implementing ATS-Proto involved several iterations. The first trial started at the end of 2002 and continued through much of 2003. The second trial started immediately after the first one ended and then continued into 2004. By the beginning of Summer 2004, the realization that imperative programming in ATS should be built on top of PwTP (programming-with-theorem-proving) set off the third trial of implementing ATS, which resulted in a functioning typechecker in July 2004 and a functioning interpreter by the end of 2004. The fourth trial started during the first half of 2005 and continued throughout 2006, finally leading to ATS-Proto. There was yet another trial, the fifth one, but it was soon abandoned. For learning more details about the development of ATS-Proto, please find the code written for each of the mentioned trial versions on-line. The conservative mark-sweep garbage collector included in the runtime of ATS-Proto was written by Rick Lavoe.

The implementation of ATS-Geizella started in Fall 2006 and it became functioning by Summer 2007. Unlike ATS-Proto, there was no longer support in ATS-Geizella for interpreting ATS code. With ATS-Geizella being ready for use, the development of ATS reached the point where the natural step to take next would be to make ATS capable of boostrapping itself.

The implementation of ATS-Anairiats started in Summer 2007. By the middle of May 2008, ATS-Anairiats succeeded in compiling itself into a set C-files that could be further compiled into an excutable by a standard C-compiler such as gcc. After about 5 and one-half years of continuing effort, the development of ATS finally reached the milestone where the language was able to bootstrap itself.

The support for templates was an "add-on" in ATS-Anairiats. It was not properly designed and could cause acute problems in programming. The primary motivation for designing and implementing ATS-Postiats (ATS2) was to greatly improve the support for template-based programming in ATS. The implementation of ATS-Postiats started in March 2010. It took 2 years and 3 months to produce a running typechecker for ATS-Postiats. In total, it took 3 years and 6 months for the first version of ATS-Postiats to be officially released at the end of August, 2013.

This page is created by Hongwei Xi
with tools including ATS/weboxy, atscc2js and atscc2php.