ATS is a statically typed programming language with a functional programming core inspired by ML.
Aiming at unifying implementation with formal specification, ATS is equipped with a highly expressive type system rooted in the framework Applied Type System, which in turn gives the language its name. In particular, ATS supports practical use of both dependent types and linear types in capturing program invariants. Moreover, ATS supports a form of embeddable templates in the sense that such a template may be implemented inside the body of a function (so as to allow the implementation to have direct access to the arguments of the function), greatly facilitating code reuse.
There is also a subsystem ATS/LF in ATS for accommodating 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.