Skip to content
Hongwei Xi edited this page Sep 1, 2020 · 47 revisions

Welcome to the wiki for ATS2.

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

The programming language ATS is a statically typed language with a type system rooted in the framework Applied Type System. ATS unifies implementation with formal specification 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.

ATS2 is implemented in ATS1, which is implemented in itself. The compiler for ATS2 is given the name ATS-Postiats, and it is currently containing about 180K lines of code.

The official website of ATS is at, which is built using ATS itself. For a thorough introduction to ATS, please see the book Introduction to Programming in ATS and A Tutorial on Programming Features in ATS. Also, there is a google-group-forum for discussing any and all of the issues on or related to ATS.

This wiki contains the following pages.

Also of interest:

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.