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 150K 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:
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).
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.
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.
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
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.
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:
This page is created by
with tools including ATS/weboxy, atscc2js and atscc2php.