The following links are listed to allow for access to some code used in the on-line book Introduction to Programming in ATS. If the name of a file mentioned in a link is followed by the symbol (c), then the code contained in the file can be typechecked on-line. If the name is followed by (js), then the code can be first typechecked and then compiled into Javascript for execution in the browser.

Chapter: Start

Chapter: Elements of Programming

Chapter: Functions

Chapter: Datatypes

Chapter: Parametric Polymorphism

Chapter: Effectful Programming Features

Chapter: Introduction to Dependent Types

Chapter: Datatype Refinement

Chapter: Theorem-Proving in ATS/LF

Chapter: Programming with Theorem-Proving

This page is created with ATS by Hongwei Xi and also maintained by Hongwei Xi. Logo