In computing, ATS (Applied Type System) is a multi-paradigm, general-purpose, high-level, functional programming language.

ATS has support for combining theorem proving with practical programming through the use of advanced type systems.

[3] By using theorem proving and strict type checking, the compiler can detect and prove that its implemented functions are not susceptible to bugs such as division by zero, memory leaks, buffer overflow, and other forms of memory corruption by verifying pointer arithmetic and reference counting before the program runs.

Also, by using the integrated theorem-proving system of ATS (ATS/LF), the programmer may make use of static constructs that are intertwined with the operative code to prove that a function conforms to its specification.

According to the author, ATS was inspired by Martin-Löf's constructive type theory, which was originally developed for the purpose of establishing a foundation for mathematics.

This is likely due to the steep learning associated with ATS, which is present because of the language's use of dependent type-checking and template instance resolution.

[5] The main focus of ATS is to support formal verification via automated theorem proving, combined with practical programming.

It incorporates a system similar to those of proof assistants which usually only aim to verify mathematical proofs—except ATS uses this ability to prove that the implementations of its functions operate correctly, and produce the expected output.

The benefit of the ATS system is that since all theorem proving occurs strictly within the compiler, it has no effect on the speed of the executable program.

Garbage collection is not used unless explicitly stated with -D_ATS_GCATS )[9] compiles and gives the expected result as in case+, val+, type+, viewtype+, ... Dataviews are often declared to encode recursively defined relations on linear resources.