./lang/ats2, Functional programming language with dependent types

[ CVSweb ] [ Homepage ] [ RSS ] [ Required by ] [ Add to tracker ]

Branch: CURRENT, Version: 0.4.2nb1, Package name: ats2-0.4.2nb1, Maintainer: pkgsrc-users

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.

Master sites:

Filesize: 4424.77 KB

Version history: (Expand)

CVS history: (Expand)


   2023-01-16 05:38:04 by David A. Holland | Files touched by this commit (1) 
Log message:
lang/ats2: USE_TOOLS+=find, install fails using solaris's
   2022-05-15 00:25:42 by David A. Holland | Files touched by this commit (90) 
Log message:
Bump all elisp packages for the CONFLICTS change.
   2022-04-17 20:48:17 by Thomas Klausner | Files touched by this commit (1) 
Log message:
ats2: PLIST_VARS needs to be defined unconditionally

Fixes build with emacs option turned off (the default)
   2022-04-14 22:13:19 by Nikita | Files touched by this commit (4) 
Log message:
ats2: Build emacs mode.
   2022-04-14 19:29:11 by Nikita | Files touched by this commit (5) 
Log message:
lang/ats2: Add version 0.4.2

Import from wip/ats2 by Atsushi Toyokura, Mateusz Poszwa.

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.