Some Basics on ATS ATS consists of a static component (statics), where types are formed and reasoned about, and a dynamic component (dynamics), where programs are constructed and evaluated. Some Primitive Sorts and Constants The statics of ATS is a simply typed language. The types for terms in the statics are called sorts (so as to avoid potential confusion with the types for terms in the dynamics) and the terms in it are called static terms. We use sigma for sorts and s for static term. The primitive sorts in ATS include bool, int, prop, type, view and viewtype. There are also some primitive constants c in the statics, each of which is assigned a constant sort (or c-sort, for short) of the following form:
tt is an implementation of the constructive and predicative theory of dependent types (also known as Martin-Löf type theory) in the programing language C. It is an experiment in using Arthur Whitney's programming style. The second release of the program, version 1.0 beta is now available for testing.