zbMATH — the first resource for mathematics

Generalizing Automath by means of a lambda-typed lambda calculus. (English) Zbl 0648.68099
Mathematical logic and theoretical computer science, Lect. Notes Pure Appl. Math. 106, 71-92 (1987).
Summary: [For the entire collection see Zbl 0642.00005.]
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 will 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.

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B40 Combinatory logic and lambda calculus