INT2PROGINATS-CODE

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

• hello.dats(c)
• hello.dats(js)
• queens.dats(c)
• queens.dats(js)

Chapter: Elements of Programming

• misc.dats(c)

Chapter: Functions

• misc.dats(c)
• acker.dats(c)
• acker.dats(js)
• bsearch.dats(c)
• bsearch.dats(js)
• coinchange.dats(c)
• coinchange.dats(js)
• queens.dats(c)
• queens.dats(js)
• twice.dats(c)
• twice.dats(js)

Chapter: Datatypes

• misc.dats(c)
• intexp.dats(c)
• intexp.dats(js)

Chapter: Parametric Polymorphism

• misc.dats(js)
• listfuns.dats(js)
• mergesort.dats(js)

Chapter: Effectful Programming Features

• misc.dats(c)
• counter.dats(c)
• counter.dats(js)
• hello.dats(c)
• echoline.dats(c)
• permord.dats(c)
• montecarlo.dats(c)

Chapter: Introduction to Dependent Types

• misc.dats(c)

Chapter: Datatype Refinement

• misc.dats(c)
• listfuns.dats(c)
• mergesort.dats(c)
• rbtree.dats(c)

Chapter: Theorem-Proving in ATS/LF

• misc.dats(c)
• tree.dats(c)
• brauntree.dats(c)

Chapter: Programming with Theorem-Proving

• misc.dats(c)
• ifact.dats(c)
• ifact.dats(js)
• ifact23.dats(c)
• ifact23.dats(js)

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