The name "type theory" has been given to several theories that can be classified in two rough categories: the early type theories of Russell, Ramsey, Church, ... and the modern type theories of de Bruijn, Martin-Löf, Coquand and Huet, Paulin, ... A characteristic property of the modern type theories is that proofs are objects of the theory, while they are not in the early type theories. The early type theories have been developed from the beginning of the 20 th century to the publication of Church's paper, in 1940, and the modern ones from the first version of Automath, in 1967, to current time. Gödel's system T has been published in Gödel's 1958 paper, but according to Troelstra's introductory note to this paper, the ideas date back to 1941. A revised version of the paper has been written by Gödel between 1965 and 1972 and Tait's paper on system T has been published in 1967. Thus Gödel's system T has been developed exactly at the time of the transition between early and modern type theories.