依存型と定理証明で「正しいプログラム」を書く、ATS言語入門書

Introduction to Programming in ATS

Hongwei Xi氏によるATS言語の入門書。基本的な関数型プログラミングから、単純型、再帰的データ型、多相型、依存型、線形型、定理証明、そして定理証明を伴うプログラミング（PwTP）やテンプレートベースのプログラミングまで、ATSの中核機能を体系的に解説する。プログラミング経験が乏しい読者にはやや密度が高い内容となっている。