ATS
{{language |exec=machine |gc=allowed |safety=safe |parampass=both |checking=static |strength=strong |express=explicit |tags=ATS |bnf=http://ats-lang.sourceforge.net/htdocs-old/DOCUMENT/GRAMMAR/ats_grammar_desc.html |site=http://www.ats-lang.org/ |hopl=no }} {{language programming paradigm|Declarative}} {{language programming paradigm|Functional}} {{language programming paradigm|Imperative}} {{language programming paradigm|Concurrent}} {{language programming paradigm|Modular}} '''ATS''' is a [[Type checking|statically typed]] programming language that unifies implementation with formal specification. It is equipped with a highly expressive [[type system]] rooted in the framework Applied Type System, which gives the language its name. In particular, both dependent types and linear types are available in ATS.
-
[[Functional programming]]. The core of ATS is a functional language based on eager (aka. call-by-value) evaluation, which can also accommodate lazy (aka. call-by-need) evaluation. The availability of linear types in ATS often makes functional programs written in it run not only with surprisingly high efficiency (when compared to [[C]]) but also with surprisingly small (memory) footprint (when compared to [[C]] as well).
-
[[Imperative programming]]. The novel and unique approach to imperative programming in ATS is firmly rooted in the paradigm of programming with theorem-proving. The type system of ATS allows many features considered dangerous in other languages (e.g., explicit pointer arithmetic and explicit memory allocation/deallocation) to be safely supported in ATS, making ATS a viable programming langauge for low-level systems programming.
-
[[Concurrent programming]]. ATS can support multithreaded programming through safe use of pthreads. The availability of linear types for tracking and safely manipulating resources provides an effective approach to constructing reliable programs that can take great advantage of multicore architectures.
-
[[Modular programming]]. The module system of ATS is largely infuenced by that of [[Modula-3]], which is both simple and general as well as effective in supporting large scale programming.
In addition, ATS contains a subsystem ATS/LF that supports a form of (interactive) theorem-proving, where proofs are constructed as total functions. With this component, ATS advocates a programmer-centric approach to program verification that combines programming with theorem-proving in a syntactically intertwined manner. Furthermore, this component can serve as a logical framework for encoding deduction systems and their (meta-)properties.
==Citations==
- [[wp:ATS_%28programming_language%29|Wikipedia:ATS (programming language)]]