Introduction to Programming in ATS:
PrevNext

III. Programming with Dependent Types

Table of Contents
9. Introduction to Dependent Types
10. Datatype Refinement
11. Theorem-Proving in ATS/LF
12. Programming with Theorem-Proving
PrevHomeNext
Example: Constructing a Statically Allocated List Introduction to Dependent Types