Home

Welcome to the wiki for ATS2.

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

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.

The official website of ATS is at http://ats-lang.org, 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 the issues on or related to ATS.

This wiki contains the following pages.

• Frequently asked questions.
• Building and installing.
• Editors and IDEs
• ATS code style: style guide, detecting and avoiding memory leaks, code optimization, design patterns.
• 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 and terminology in ATS: char, dataviewtype, overload, sort, type.
• Wiki TODO: A list of wiki pages that need the most help.
• Docker Image Generation and Deployment
• 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.