# Category:ATS

**ATS**

This

**programming language**may be used to instruct a computer to perform a task.

Official website |
---|

Execution method: | Compiled (machine code) |
---|---|

Garbage collected: | Allowed |

Parameter passing methods: | By reference, By value |

Type safety: | Safe |

Type strength: | Strong |

Type expression: | Explicit |

Type checking: | Static |

Lang tag(s): | ATS |

See Also: |

**ATS** is a 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.

## CitationsEdit

## Subcategories

This category has the following 3 subcategories, out of 3 total.

### @

- ATS examples needing attention (empty)
- ATS Implementations (empty)
- ATS User (empty)

## Pages in category "ATS"

The following 104 pages are in this category, out of 104 total.

### A

### C

- Compiler/AST interpreter
- Compiler/code generator
- Compiler/lexical analyzer
- Compiler/syntax analyzer
- Compiler/virtual machine interpreter
- Compound data type
- Continued fraction
- Continued fraction/Arithmetic/Construct from rational number
- Continued fraction/Arithmetic/G(matrix ng, continued fraction n)
- Continued fraction/Arithmetic/G(matrix ng, continued fraction n1, continued fraction n2)
- Convex hull

### D

### G

### H

### R

### S

- Self-hosting compiler
- Sequence of primes by trial division
- Set
- Sierpinski triangle
- Sierpinski triangle/Graphical
- Singly-linked list/Element definition
- Singly-linked list/Element insertion
- Singly-linked list/Element removal
- Singly-linked list/Traversal
- Sort a list of object identifiers
- Sort an array of composite structures
- Sort disjoint sublist
- Sort numbers lexicographically
- Sort using a custom comparator
- Sorting algorithms/Counting sort
- Sorting algorithms/Insertion sort
- Sorting algorithms/Merge sort
- Sorting algorithms/Patience sort
- Sorting algorithms/Quicksort
- Sorting algorithms/Radix sort
- Sorting algorithms/Shell sort
- Sorting algorithms/Tree sort on a linked list
- Stack
- Stream merge
- Sum digits of an integer
- Sutherland-Hodgman polygon clipping