This book starts from the core of ATS, a statically typed call-by-value
functional programming language, gradually introducing the reader to
dependent types, linear types and the paradigm of programming with
theorem-proving. It assumes no familiarity of the reader with functional
programming but it does expect the reader to have already acquired
basic understanding of programming and possibly some programming skills.
The primary purpose of this tutorial is to bring insights into a rich
set of programming features in ATS and also demonstrate through concrete
examples that these features can be made of effective use in the
construction of high-quality programs. For someone familiar with both ML
and C, it is possible to learn programming in ATS by simply studying the
tutorial. However, a coherent and systematic view of ATS is diffcult to be
gained from the tutorial alone.
This book consists of a set of lecture notes for a crash course on
functional programming in ATS. The primary focus of these notes is set
upon advocating a style of problem-solving that makes extensive use of
list-processing and stream-processing functions. After finishing
this course, one will have become familiar with recursion in problem-solving
and ready to formulate high-level combinator-based programming solutions.
Please find
on-line
(backup)
various (short) programs in ATS plus detailed explanation that are written
for the purpose of advocating effective programming in ATS.
