Generalizing Automath by means of a lambda-typed lambda calculus

The calculus delta conjunction 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 will not be considered in this paper. The calculus deal 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 correcntess 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 Book