ABSTRACT
The calculus developed in this paper is claimed to be able to embrace all the essential aspects of Automath, apart from the feature of type inclusion, which wili. not be considered in this paper. The calculus deals with a correctness notion for lambda-typed lambda formulas (which are presented in the form of what will be called lambda trees). To an Automath book there corresponds a single lambda tree, and the correctness of the book is equivalent to the correctness of the tree. The algorithmic definition of correctness of lambda trees corresponds to an efficient checking algorithm for Automath books.
