The ATS Programming Language

Unleashing the Potential of Types!

  • What is ATS?
  • What is ATS good for?
  • Acknowledgments
  • Download and Installation: The current stable release is ats-lang-anairiats-0.2.7 (2.4MB)
  • Some Simple ATS Programs

  • What is ATS?

    ATS is a programming language that unifies specification and implementation. It is equipped with an expressive type system rooted in the framework Applied Type System, which gives the language its name. In particular, both dependent types and linear types are available in ATS. The current implementation of ATS (ATS/Anairiats) is written in ATS itself. It can be as efficient as C/C++ (see The Computer Language Benchmarks Game for concrete evidence) and supports a variety of programming paradigms that include:

    • Functional programming. While ATS is primarily a language based on eager (aka. call-by-value) evaluation, it also supports lazy (aka. call-by-need) evaluation. The availability of linear types in ATS can often make functional programs in ATS not only run with surprisingly high efficiency (when compared to C) but also run with surprisingly small (memory) footprint (when compared to C as well).

    • Imperative programming. The novel and unique approach to imperative programming in ATS is firmly rooted in the paradigm of programming with theorem proving. While features considered dangerous in other languages (e.g., explicit pointer arithmetic and explicit memory allocation/deallocation) are allowed in ATS, the type system of ATS is still able to guarantee that no run-time errors can occur that may lead to memory corruption.

    • Concurrent programming. ATS, equipped with a multicore-safe implementation of garbage collection, can support multithreaded programming through the use of pthreads. There is also high-level support in ATS for parallel let-binding, which provides a simple and effective means to constructing programs that can take advantage of multicore architectures.

    • Modular programming. The module system of ATS is largely infuenced by that of Modula-3, which is both simple and general as well as effective in supporting large scale programming.

    In addition, ATS contains a component ATS/LF that supports a form of (interactive) theorem proving, where proofs are constructed as total functions. With this component, ATS advocates a programmer-centric approach to program verification that combines programming with theorem proving. Furthermore, this component may be used as a logical framework to encode various deduction systems and their (meta-)properties.

  • What is ATS good for?

  • ATS can enforce great precision in practical programming.
  • ATS allows the programmer to write efficient functional programs by taking advantage of native unboxed data representation.
  • ATS allows the programmer to reduce the memory footprint of a program by making use of linear types.
  • ATS allows the programmer to enhance the safety (and efficiency) of a program by making use of theorem proving.
  • ATS allows the programmer to write safe low-level code that runs in OS kernels.
  • ATS can help teach type theory, allowing students to see first-handedly how advanced types such as dependent types and linear types can be effectively employed in practical programming.
  • Acknowledgments

    The development of ATS has been funded in part by National Science Foundation under the grants no. CCR-0081316/CCR-0224244, no. CCR-0092703/0229480, no. CNS-0202067 and no. CCF-0702665. As always, any opinions, findings, and conclusions or recommendations expressed here are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.

    Many people worked on ATS in the past. The names of some of these people are included in the following list:

    Chiyan Chen, Sa Cui, Matthew Danish, Kevin Donnelly, Rick Lavoie, Likai Liu, Michel Machado, Zhiqiang Ren, Rui Shi, Hongwei Xi, Dengping Zhu

  • Download and Installation

    ATS is Open Source and Free Software, and it is freely available under the GNU GENERAL PUBLIC LICENSE version 3 (GPLv3 ) as is published by the Free Software Foundation. The current implementation of ATS is given the name ATS/Anairiats or simply Anairiats.


    In order to install ATS, the following requirements need to be met:
  • Operating System requirement: ATS is supported under the following operating systems:
    • Linux
    • Windows with Cygwin
    • MacOS X (currently no GC support for multithreading)
    • SunOS (currently no GC support for multithreading)
    • BSD Unix (currently no GC support for multithreading)
  • Programming Language requirement: GNU C Compiler (GCC).
  • We plan to port ATS to other platforms in the future. If you have succeeded in porting ATS to a platform not listed here, please drop us a note.

    The GMP library (libgmp.a), which is in general included in a GNU/Linux distribution, is currently optional and it may be required for installing a release of ATS in the future. Please see for more details on GMP.

    Installation from a precompiled package

    This installation method currently only supports the following platforms:

    • Linux on i386 (x86-32)
    • Linux on AMD64 (x86-64)
    • SunOS on UltraSparc

    Please first download a compressed tarball containing a precompiled release of ATS from the following site that suits your platform:

    Let "x.x.x" be the version number of the downloaded ATS package.

    (METHOD 1) You can untar the tarball in the root directory "/" and then set the shell environment variables ATSHOME and ATSHOMERELOC to "/usr/share/atshome" and "ATS-x.x.x", respectively. This method most likely requires root access.

    (METHOD 2) You can untar the tarball in the directory "/tmp", and then move the directory "/tmp/usr/share/atshome" into a directory of your choice, say, "FOO", and then set the environment variables ATSHOME and ATSHOMERELOC to "FOO/atshome" and "ATS-x.x.x", repectively. In addition, you need to put "$ATSHOME/bin" on your execution path or create symbolic links to the executables $ATSHOME/bin/atscc and $ATSHOME/bin/atsopt in a directory that is already on your execution path.

    Installation through source code compilation

  • Step 1:

    After downloading a compressed tarball containing a release of ATS from the following site:

    please untar it in a directory, say "FOO", of your choice. This, for instance, can be done by executing the following command line:

    tar -zvxf ATS.tar.gz 
    All the files and directories extracted from the tarball are now in the directory "FOO/ATS".
  • Step 2:

    Please execute the following command
    ./configure --prefix=DESTDIR
    where DESTDIR is the name of the directory where ATS is to be installed. If the argument [--prefix=DESTDIR] is missing, then the default directory for installing ATS is "/usr/local". You can now go into the directory "FOO/ATS" and execute
    make all
    This generates executables "atscc" and "atsopt" in the directory "FOO/ATS/bin", which are the commands you need for compiling ATS programs, and a library file "libats.a" in the directory "FOO/ATS/CCOMP/lib", which you need for linking.
  • Step 3:

    Please set the environment variable ATSHOME to "FOO/ATS" and then set the environment variable ATSHOMERELOC to "ATS-x.x.x", where x.x.x is the version number of the compiled ATS package.
  • Step 4:

    Optionally, you may install ATS by executing the following command line:
    make install
    and then set ATSHOME to $DESTDIR/share/ats-anairiats-x.x.x, which is the name of the directory where ATS is installed. The environment variable ATSHOMERELOC is still set to "ATS-x.x.x".

  • Installation through bootstrapping

    This installation method is probably the best if you would like to keep abreast of the development of ATS. Please find more details here.
  • Some Simple ATS Programs

    Let us now construct and compile some simple ATS programs.

    Hello, world!

    In a file named HelloWorld.dats, we write the following lines of code
    // compilation command:
    //   atscc -o HelloWorld HelloWorld.dats
    implement main () = begin
      print ("Hello, world!"); print_newline ()
    By executing the following command line, we produce an excutable file named "HelloWorld":
    atscc -o HelloWorld HelloWorld.dats
    What happens here is that atscc first compiles HelloWorld.dats into HelloWorld_dats.c, which is then compiled by gcc to produce "HelloWorld". By running "HelloWorld", we can see the following line on the standard output:
    Hello, world!

    Computing Fibonacci Numbers

    We now present a simple example to illustrate the idea of programming with theorem-proving.

    We can specify a function fib as follows for computing Fibonacci numbers:

    fib(0)   = 0
    fib(1)   = 1
    fib(n+2) = fib(n) + fib(n+1) for n >= 0
    A direct implementation of this specification in ATS can be done as follows:
    fun fib (n: int): int =
      if n = 0 then 0 else if n = 1 then 1 else fib (n-2) + fib(n-1)
    // end of [fib]
    Clearly, this is a terribly inefficient implementation of exponential time-complexity. An implementation of fib in C is given as follows that is of linear time-complexity:
    int fibc (int n) {
      int tmp, f0 = 0, f1 = 1 ;
      while (n-- > 0) { tmp = f1 ; f1 = f0 + f1 ; f0 = tmp ; } ; return f0 ;
    } // end of [fibc]
    There is obviously a logic gap between the defintion of fib and its implementation fibc in C. In ATS, we can give an implementation of fib that completely bridges this gap. First, we need a way to encode the definition of fib into ATS, which is fulfilled by the declaration of the following dataprop:
    dataprop FIB (int,int) =
      | FIB0 (0,0) | FIB1 (1,1)
      | {n:nat} {r0,r1:int} FIB2 (n+2,r0+r1) of (FIB (n,r0), FIB (n+1,r1))
    // end of [FIB]
    This declaration introduces a type FIB for proofs. Such a type is referred to as a prop in ATS. Intuitively, if a proof can be assgined the type FIB(n,r) for some integers n and r, then fib(n) equals r. In other words, FIB(n,r) encodes the relation fib(n)=r. There are three constructors FIB0, FIB1 and FIB2 associated with FIB, which are given the following types corresponding to the three equations in the definition of fib:
    FIB0 : () -> FIB (0, 0)
    FIB1 : () -> FIB (1, 1)
    FIB2 : {n:nat} {r0,r1:int} (FIB (n, r0), FIB (n, r1) -> FIB (n+2, r0+r1)
    Note that {...} is the concrete syntax in ATS for universal quantification. For instance, FIB2(FIB0(), FIB1()) is a term of the type FIB(2,1), attesting to fib(2)=1.

    We now implement a function in ATS as follows for computing Fibonacci numbers:

    fun fibats {n:nat} (n: int n)
      : [r:int] (FIB (n, r) | int r) = let
      fun loop {n,i:nat | i <= n} {r0,r1:int} .<n-i>. (
        pf0: FIB (i, r0), pf1: FIB (i+1, r1) | r0: int (r0), r1: int (r1), ni: int(n-i)
      ) : [r:int] (FIB (n, r) | int (r)) =
      if ni > 0 then
        loop {n,i+1} (pf1, FIB2 (pf0, pf1) | r1, r0+r1, ni-1)
      else (pf0 | r0)
      loop (FIB0(), FIB1() | 0, 1, n)
    end // end of [fibats]
    Note that fibats is assigned the following type:
    fibats : {n:nat} int(n) -> [r:int] (FIB(n,r) | int(r))
    where [...] is the concrete syntax in ATS for existential quantification and the bar symbol (|) is just a separator (like a comma) for separating proofs from values. For each integer I, int(I) is a singleton type for the only integer whose value is I. When fibats is applied to an integer of value n, it returns a pair consisting of a proof and an integer value r such that the proof, which is of the type FIB(n,r), asserts fib(n)=r. Therefore, fibats is a verified implementation of fib. Note that the loop function directly corresponds to the while-loop in the body of fibc.

    Lastly, we emphasize that proofs are completely erased after typechecking. In particular, there is no proof construction at run-time.

    List Quicksort

    This one is for program verification enthusiasts: An implementation of list quicksort is given here that guarantees solely based on its type that the implmentation is terminating and the output list it returns is always a sorted permutation of its input list. This is considered a milestone example in the development of ATS.

    A GTK/cairo Clock

    A clock implementation based on GTK+ and cairo is available here, which demonstrates some simple and effective use of linear types in ATS for tracking resources statically, that is, at compile-time.

    More Examples

    Please find more, more advanced and larger, examples here.

  • Resources for Programming in ATS

    Please follow the link to find the User's Guide on ATS/Anairiats, an Emacs mode for ATS, a variety of contributed code, and more.

  • This page is maintained by Hongwei Xi. As always, your comments are welcome. Logo