ATS

ATS, aka Applied Type System, is an open source programming language created in 2013 by Hongwei Xi.

#283on PLDB

11Years Old

217Repos

Try now: Riju

ATS (Applied Type System) is a programming language designed to unify programming with formal specification. ATS has support for combining theorem proving with practical programming through the use of advanced type systems. A past version of The Computer Language Benchmarks Game has demonstrated that the performance of ATS is comparable to that of the C and C++ programming languages. Read more on Wikipedia...

ATS website
ATS Wikipedia page
There are at least 217 ATS repos on GitHub
ATS first developed in Boston University
file extensions for ATS include dats, hats and sats
The Google BigQuery Public Dataset GitHub snapshot shows 26 users using ATS in 46 repos on GitHub
Explore ATS snippets on Rosetta Code
Monaco package for syntax highlighting ATS
GitHub supports syntax highlighting for ATS
ats-lang.org was registered in 2007
See also: (4 related languages)DML, ML, OCaml, C

Example from Riju:

val _ = print ("Hello, world!\n")
implement main0 () = ()

Example from the Hello World Collection:

// Hello world in ATS

implement main () = begin
  print ("Hello, world!"); print_newline ()
end

Example from Linguist:

(* ****** ****** *)
//
// HX-2013-11
//
// Implementing a variant of
// the problem of Dining Philosophers
//
(* ****** ****** *)
//
#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"
//
(* ****** ****** *)

staload "{$LIBATSHWXI}/teaching/mythread/SATS/mythread.sats"

(* ****** ****** *)

local
//
#include "{$LIBATSHWXI}/teaching/mythread/DATS/mythread.dats"
//
in (* in of [local] *)
//
// HX: it is intentionally left to be empty
//
end // end of [local]

(* ****** ****** *)

local
//
#include "{$LIBATSHWXI}/teaching/mythread/DATS/mythread_posix.dats"
//
in (* in of [local] *)
//
// HX: it is intentionally left to be empty
//
end // end of [local]

(* ****** ****** *)

(* end of [DiningPhil2_thread.dats] *)

Example from Wikipedia:

#define BUFLEN 10
var !p_buf with pf_buf = @[byte][BUFLEN](0)    // pf_buf = @[byte][BUFLEN](0) @ p_buf[14]

ATS Keywords

abstype abst0ype absprop absview absvtype absviewtype absvt0ype absviewt0ype as and assume begin classdec datasort datatype dataprop dataview datavtype dataviewtype do end extern extype extvar exception fn fnx fun prfn prfun praxi castfn if then else ifcase in infix infixl infixr prefix postfix implmnt implement primplmnt primplement import let local macdef macrodef nonfix symelim symintr overload of op rec sif scase sortdef sta stacst stadef static staload dynload try tkindef typedef propdef viewdef vtypedef viewtypedef prval var prvar when where with withtype withprop withview withvtype withviewtype

Feature	Supported	Token	Example
Conditionals	✓
Functions	✓
MultiLine Comments	✓	(* *)	(* A comment *)
Comments	✓		// A comment
Line Comments	✓	//	// A comment
Semantic Indentation	X

ATS - Programming language

Language features