Anonymous user
Category:ATS: Difference between revisions
ATS info
(Stub, guess at type expression, official site, does not appear to be on HOPL) |
(ATS info) |
||
Line 1:
|exec=machine
|express=implicit▼
|gc=allowed
|safety=safe
|parampass=both
|checking=static
|strength=strong
|tags=ats
|bnf=http://www.ats-lang.org/DOCUMENTATION/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, equipped with a multicore-safe implementation of [[garbage collection]], can support multithreaded programming through the use of pthreads. The availability of linear types for tracking and safely manipulating resources provides a effective means to constructing reliable programs that can take 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)]]
| |||