The literature most closely related to this comes from Martin-Löf [Martin-Löf 73,Martin-Löf 82] and the Swedish computer scientists at Goteborg who are concerned with making type theory a usable formalism [Nordstrom 81,Nordstrom & Petersson 83,Nordstrom & Smith 84]. The AUTOMATH work at Eindhoven in The Netherlands is also closely related [deBruijn 80,Jutting 79,van Daalen 80,Zucker 75], as is the work at INRIA [Coquand & Huet 85]. In fact, deBruijn's ideas are direct predecessors of those in Martin-Löf 's writings with intermediate refinements from Scott [Scott 70]. One can see in deBruijn's work the influence of his fellow mathematician and countryman, L. E. J. Brouwer, the founder of Intuitionism [Brouwer 23] . We will examine some of these influences below as well as trace the influence of more recent research such as the work of J. L. Bates [Bates 79] and Constable [Constable 71,Constable & Zlatin 84,Constable 85].