Debian Bug report logs - #725033
ITP: ats2-lang -- ATS (v2) is a statically typed programming language that unifies implementation with formal specification.

Package: wnpp; Maintainer for wnpp is wnpp@debian.org;

Reported by: Matthew Danish <mrd@debian.org>

Date: Mon, 30 Sep 2013 18:45:02 UTC

Owned by: Matthew Danish <mrd@debian.org>

Severity: wishlist

Tags: pending

Reply or subscribe to this bug.

Toggle useless messages

View this report as an mbox folder, status mbox, maintainer mbox


Report forwarded to debian-bugs-dist@lists.debian.org, debian-devel@lists.debian.org, wnpp@debian.org:
Bug#725033; Package wnpp. (Mon, 30 Sep 2013 18:45:06 GMT) Full text and rfc822 format available.

Acknowledgement sent to Matthew Danish <mrd@debian.org>:
New Bug report received and forwarded. Copy sent to debian-devel@lists.debian.org, wnpp@debian.org. (Mon, 30 Sep 2013 18:45:06 GMT) Full text and rfc822 format available.

Message #5 received at submit@bugs.debian.org (full text, mbox):

From: Matthew Danish <mrd@debian.org>
To: Debian Bug Tracking System <submit@bugs.debian.org>
Subject: ITP: ats2-lang -- ATS (v2) is a statically typed programming language that unifies implementation with formal specification.
Date: Mon, 30 Sep 2013 14:29:12 -0400
Package: wnpp
Severity: wishlist
Owner: Matthew Danish <mrd@debian.org>

* Package name    : ats2-lang
  Version         : 0.0.3
  Upstream Author : Hongwei Xi <hwxi@cs.bu.edu>
* URL             : http://www.ats-lang.org/
* License         : GPL
  Programming Lang: ATS, C
  Description     : ATS (v2) is a statically typed programming language that unifies implementation with formal specification.

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. The
current implementation of ATS (ATS/Anairiats) is written in ATS itself. It can
be as efficient as C/C++ (see The Computer Language Benchmarks Game for
concrete evidence) and supports a variety of programming paradigms that
include:

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 language 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 an 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.

ATS2 is the second major version of ATS, a complete rewrite of the compiler system.



Added tag(s) pending. Request was from Anibal Monsalve Salazar <anibal@debian.org> to control@bugs.debian.org. (Fri, 11 Oct 2013 19:06:05 GMT) Full text and rfc822 format available.

Send a report that this bug log contains spam.


Debian bug tracking system administrator <owner@bugs.debian.org>. Last modified: Sat Apr 19 12:40:20 2014; Machine Name: buxtehude.debian.org

Debian Bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.