Introduction to Programming in ATS:
<<< Previous		Next >>>

III. Dependent Types for Programming

Table of Contents
Introduction to Dependent Types
Datatype Refinement
Theorem-Proving in ATS/LF
Programming with Theorem-Proving
Summary

<<< Previous	Home	Next >>>
Summary		Introduction to Dependent Types