Characteristics of de Bruijn's early proof checker Automath

The `mathematical language' Automath, conceived by N.G. de Bruijn in 1968,was the first theorem prover actually working and was used for checking manyspecimina of mathematical content. Its goals and syntactic ideas inspired Th.Coquand and G. Huet to develop the calculus of constructions, CC, which was oneof the first widely used interactive theorem provers and forms the basis forthe widely used Coq system. The original syntax of Automath is not easy tograsp. Yet, it is essentially based on a derivation system that is similar tothe Calculus of Constructions (`CC'). The relation between the Automath syntaxand CC has not yet been sufficiently described, although there are manyreferences in the type theory community to Automath. In this paper we focus onthe backgrounds and on some uncommon aspects of the syntax of Automath. Weexpose the fundamental aspects of a `generic' Automath system, encapsulatingthe most common versions of Automath. We present this generic Automath systemin a modern syntactic frame. The obtained system makes use of {\lambda}D, adirect extension of CC with definitions