ATS - Programming language

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

#471on PLDB

11Years Old

217Repos

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...

Tags: programming language
There are at least 217 ATS repos on GitHub
Early development of ATS happened in Boston University
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

Language features

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