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. 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 subsystem, ATS is able to advocate a programmer-centric approach to program verification that combines programming with theorem-proving in a syntactically intertwined manner. Furthermore, ATS/LF can also serve as a logical framework (LF) for encoding various formal systems (such as logic systems and type systems) together with proofs of their (meta-)properties.
OS | Architecture | Version |
---|---|---|
NetBSD 10.0 | aarch64 | ats2-0.4.2nb1.tgz |
NetBSD 10.0 | aarch64 | ats2-0.4.2nb1.tgz |
NetBSD 10.0 | aarch64 | ats2-0.4.2nb1.tgz |
NetBSD 10.0 | aarch64eb | ats2-0.4.2nb1.tgz |
NetBSD 10.0 | aarch64eb | ats2-0.4.2nb1.tgz |
NetBSD 10.0 | alpha | ats2-0.4.2nb1.tgz |
NetBSD 10.0 | alpha | ats2-0.4.2nb1.tgz |
NetBSD 10.0 | earmv4 | ats2-0.4.2nb1.tgz |
NetBSD 10.0 | earmv6hf | ats2-0.4.2nb1.tgz |
NetBSD 10.0 | earmv6hf | ats2-0.4.2nb1.tgz |
NetBSD 10.0 | earmv6hf | ats2-0.4.2nb1.tgz |
NetBSD 10.0 | earmv7hf | ats2-0.4.2nb1.tgz |
NetBSD 10.0 | earmv7hf | ats2-0.4.2nb1.tgz |
NetBSD 10.0 | earmv7hf | ats2-0.4.2nb1.tgz |
NetBSD 10.0 | i386 | ats2-0.4.2nb1.tgz |
NetBSD 10.0 | i386 | ats2-0.4.2nb1.tgz |
NetBSD 10.0 | i386 | ats2-0.4.2nb1.tgz |
NetBSD 10.0 | m68k | ats2-0.4.2nb1.tgz |
NetBSD 10.0 | powerpc | ats2-0.4.2nb1.tgz |
NetBSD 10.0 | powerpc | ats2-0.4.2nb1.tgz |
NetBSD 10.0 | sparc64 | ats2-0.4.2nb1.tgz |
NetBSD 10.0 | sparc64 | ats2-0.4.2nb1.tgz |
NetBSD 10.0 | sparc | ats2-0.4.2nb1.tgz |
NetBSD 10.0 | sparc | ats2-0.4.2nb1.tgz |
NetBSD 10.0 | vax | ats2-0.4.2nb1.tgz |
NetBSD 10.0 | vax | ats2-0.4.2nb1.tgz |
NetBSD 10.0 | x86_64 | ats2-0.4.2nb1.tgz |
NetBSD 10.0 | x86_64 | ats2-0.4.2nb1.tgz |
NetBSD 10.0 | x86_64 | ats2-0.4.2nb1.tgz |
NetBSD 9.0 | aarch64 | ats2-0.4.2nb1.tgz |
NetBSD 9.0 | aarch64 | ats2-0.4.2nb1.tgz |
NetBSD 9.0 | aarch64 | ats2-0.4.2nb1.tgz |
NetBSD 9.0 | alpha | ats2-0.4.2nb1.tgz |
NetBSD 9.0 | alpha | ats2-0.4.2nb1.tgz |
NetBSD 9.0 | earmv4 | ats2-0.4.2nb1.tgz |
NetBSD 9.0 | earmv6hf | ats2-0.4.2nb1.tgz |
NetBSD 9.0 | earmv6hf | ats2-0.4.2nb1.tgz |
NetBSD 9.0 | earmv6hf | ats2-0.4.2nb1.tgz |
NetBSD 9.0 | earmv7hf | ats2-0.4.2nb1.tgz |
NetBSD 9.0 | earmv7hf | ats2-0.4.2nb1.tgz |
NetBSD 9.0 | earmv7hf | ats2-0.4.2nb1.tgz |
NetBSD 9.0 | i386 | ats2-0.4.2nb1.tgz |
NetBSD 9.0 | i386 | ats2-0.4.2nb1.tgz |
NetBSD 9.0 | i386 | ats2-0.4.2nb1.tgz |
NetBSD 9.0 | powerpc | ats2-0.4.2nb1.tgz |
NetBSD 9.0 | powerpc | ats2-0.4.2nb1.tgz |
NetBSD 9.0 | powerpc | ats2-0.4.2nb1.tgz |
NetBSD 9.0 | sparc64 | ats2-0.4.2nb1.tgz |
NetBSD 9.0 | x86_64 | ats2-0.4.2nb1.tgz |
NetBSD 9.0 | x86_64 | ats2-0.4.2nb1.tgz |
NetBSD 9.0 | x86_64 | ats2-0.4.2nb1.tgz |
NetBSD 9.3 | x86_64 | ats2-0.4.2nb1.tgz |
NetBSD 9.3 | x86_64 | ats2-0.4.2nb1.tgz |
Binary packages can be installed with the high-level tool pkgin (which can be installed with pkg_add) or pkg_add(1) (installed by default). The NetBSD packages collection is also designed to permit easy installation from source.
The pkg_admin audit command locates any installed package which has been mentioned in security advisories as having vulnerabilities.
Please note the vulnerabilities database might not be fully accurate, and not every bug is exploitable with every configuration.
Problem reports, updates or suggestions for this package should be reported with send-pr.