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.