About 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). ATS can be as efficient as C/C++ both time-wise and
memory-wise (see The Computer
Language Benchmarks Game for concrete evidence) and supports a variety of
programming paradigms that include:
Functional programming.
The core of ATS is a functional language based on eager
(aka. call-by-value) evaluation, which can also accommodate lazy
(aka. call-by-need) evaluation. 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 and unique 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 (e.g., explicit pointer arithmetic and explicit memory
allocation/deallocation) to be safely supported in ATS, making ATS a viable
programming language for low-level systems programming.
Concurrent programming.
ATS, equipped with a multicore-safe implementation of garbage collection,
can support multithreaded programming through the use of pthreads. The
availability of linear types for tracking and safely manipulating resources
provides an effective means to constructing reliable 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 subsystem 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 in a syntactically intertwined
manner. Furthermore, this component can serve as a logical framework for
encoding deduction systems and their (meta-)properties.
ATS can enforce great precision in practical programming.
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 concretely
the power and potential of types in constructing high-quality software.
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.
