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
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
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
with tools including ATS/weboxy, atscc2js and atscc2php.