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

What is ATS?

ATS is a statically typed programming language that unifies implementation with formal specification. It is equipped with a highly 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 ATS2 (ATS/Postiats) is written in ATS1 (ATS/Anairiats), consisting of more than 180K lines of code. ATS can be as efficient as C/C++ both time-wise and memory-wise and supports a variety of programming paradigms that include:

  • Functional programming. The core of ATS is a call-by-value functional language inspired by ML. The availability of linear types in ATS often makes functional programs written in it run not only with surprisingly high efficiency (when compared to C) but also with surprisingly small (memory) footprint (when compared to C as well).
  • Imperative programming. The novel approach to imperative programming in ATS is firmly rooted in the paradigm of programming with theorem-proving. The type system of ATS allows many features considered dangerous in other languages (such as explicit pointer arithmetic and explicit memory allocation/deallocation) to be safely supported in ATS, making ATS well-suited for implementing high-quality low-level systems.
  • Concurrent programming. ATS can support multithreaded programming through safe use of pthreads. The availability of linear types for tracking and safely manipulating resources provides an effective approach to constructing reliable programs that can take great 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 subsystem ATS/LF that supports a form of (interactive) theorem-proving, where proofs are constructed as total functions. With this subsystem, ATS is able to advocate a programmer-centric approach to program verification that combines programming with theorem-proving in a syntactically intertwined manner. Furthermore, ATS/LF can also serve as a logical framework (LF) for encoding various formal systems (such as logic systems and type systems) together with proofs of their (meta-)properties.

What is ATS good for?

  • ATS can greatly enforce precision in practical programming.
  • ATS can greatly facilitate refinement-based software development.
  • ATS allows the programmer to write efficient functional programs that directly manipulate 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, demonstrating both convincingly and concretely the power and potential of types in constructing high-quality software.

Suggestion on learning ATS

ATS is feature-rich (like C++). Prior knowledge of functional programming based on ML and imperative programming based on C can be a big plus for learning ATS. In general, one should expect to encounter many unfamiliar programming concepts and features in ATS and be prepared to spend a substantial amount of time on learning them. Hopefully, one will become a superbly confident programmer at the end who can enjoy implementing large and complex systems with minimal need for debugging.


The development of ATS has been funded in part by National Science Foundation (NSF) under the grants no. CCR-0081316/CCR-0224244, no. CCR-0092703/0229480, no. CNS-0202067, no. CCF-0702665 and no CCF-1018601. 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 NSF.

Yes, ATS can!

What is new in the community?

Would you like to try ATS on-line?

The core of ATS is a typed call-by-value functional programming language that is largely inspired by ML. For instance, the following tiny ATS program is written in a style of functional programming:

ATS is both accurate and expressive in its support for (static) typechecking. The following code demonstrates the ability of ATS in detecting out-of-bounds subscripting at compile-time:

ATS is highly effective and flexible in its support for a template-based approach to code reuse. As an example, the following code is likely to remind someone of higher-order functions but it is actually every bit of a first-order implementation in ATS:

With a functional core of ML-style and certain ad-hoc support for overloading (of function symbols), ATS can readily accommodate a typical combinator-based style of coding that is often considered a prominent signature of functional programming. The following "one-liner" solution to the famous Queen Puzzle should offer a glimpse of using combinators in ATS:

Please find on-line the entirety of this example, which is meant to showcase programming with combinators in ATS.

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