Examples in ATS/Anairiats

This website contains a variety of examples implemented in ATS/Anairiats.

Introduction

INTRO contains several simple introductory examples.

Unclassified

MISC contains a miscellaneous collection of examples implemented in ATS.

SHOOTOUT contains a set of examples taken from the site for Computer Language Shootout. The efficiency of ATS is convincingly demonstrated in many examples in this set where programs in ATS outperform their counterparts in C by clear margins.

PE contains some solutions to a set of mathematical problems posted at ProjectEuler.

While there are many solutions to these problems that are already available on-line, you can find here something of great distinction: Some solutions implemented in ATS are fully verified, that is, formal proofs are provided to attest to the correctness of these solutions. This is a style that makes ATS unique in its approach to facilitating the construction of correct programs.

Systems Programming

AUP contains some examples adapted from the book Advanced UNIX Programming (2nd edition) by Marc Rochkind.

SOCKET contains some examples implemented in ATS that involve UNIX socket programming.

Object-Oriented Programming

OOP contains some examples implemented in ATS that are of object-oriented programming style.

GUI Programming

Xlib contains some examples implemented in ATS that involve the Xlib programming.

GTK contains some examples implemented in ATS that involve GTK programming.

Parallel Programming

MULTICORE contains a set of examples in ATS that involve multicore-programming.

Graphics Programming

CAIRO contains some examples implemented in ATS that involve the cairo vector graphics library.

OpenGL contains some examples implemented in ATS that involve OpenGL programming.

SDL contains some examples implemented in ATS that involve SDL programming.

Program Verification

PCPV contains a set of examples that illustrate a programmer-centric approach to program verification.

Theorem-Proving

LF contains a set of examples encoding deduction symtems and their (meta-)properties.

This page is maintained by Hongwei Xi. As always, your comments are welcome.