ATS is a statically typed programming language that unifies implementation with formal specification. The core of ATS is ML-like, and its type system is rooted in the Applied Type System framework, which in turn gives the language its name. ATS is feature-rich and it supports dependent types (of DML-style), linear types, (embeddable) templates, programming with theorem-proving (PwTP), and more.

Welcome to #ats@stackoverflow!

ATS is a statically typed programming language that unifies implementation with formal specification. The core of ATS is ML-like, and its type system is rooted in the Applied Type System framework, which supports dependent types (of DML-style), linear types, theorem-proving and more.

As of now, the community of ATS is relatively small. We recommend that any questions pertinent to the ATS programming language be given the tag #ats. Doing so can undoubtedly benefit everyone trying to learn and use ATS. In general, questions about ATS concerning syntax, library, type system, and application should be tagged under #ats. On the other hand, suggestions, bug reports, and various discussions on language features should probably be brought to the official google-group for ATS.

Links