Home

Welcome to the wiki for ATS2.

The most recent released version of ATS2 is ATS2-0.1.1.

The programming language ATS is a statically typed language with a type system rooted in the framework Applied Type System. ATS unifies specification and implementation by accommodating a programmer-centric approach to program verification: How do we know a program being implemented correctly? We ask the programmer to demonstrate it with a proof.

ATS also has another website (built using ATS itself). For a thorough introduction to ATS, see the book Introduction to Programming in ATS.

This wiki contains the following pages.

• Frequently asked questions.
• Building and installing.
• ATS code style: style guide, detecting and avoiding memory leaks, code optimization.
• Language reference: built-in operators, dependent types, linear types, error messages, features.
• Library reference: ATSLIB, contrib, built-in datatypes, built-in functions, input and output, scientific computing, and contributed libraries.
• Extensions: writing interfaces to C libraries, ATS/LF (theorem proving).
• ATS internals: built-in constraint solving, stack and heap allocation, internal types.
• Information on specific keywords in ATS: char, dataviewtype, overload, sort, type.
• Wiki TODO: A list of wiki pages that need the most help.
• Other languages.

For the first version of ATS, there is a largely unmaintained wiki.

ATS2 is distributed under the GNU General Public License version 3 (GPLv3), or any later version.