Some Remarks About Dependent Type Theory

The goal of this chapter is to describe a calculus designed in 1984/1985. This calculus was obtained by applying the ideas introduced by N.G. de Bruijn for AUTOMATH to some functional systems created by J.-Y. Girard. There were also strong connections with the work of P. Martin-Löf. This calculus provided quite simple uniform notations for proofs and (functional) programs. Because of this simplicity and uniformity, it was possible to use it for analysing logical problems such as impredicativity, paradoxes, but also notions of computer science such as parametricity. It could also be used as the basis of implementations of proof and functional systems [29], arguably simpler, or at least competitive, with the ones that were available at the time. One main theme of this work is the importance of notations in mathematics and computer science: new questions were asked and solved only because of the use of AUTOMATH notation, itself a variation of λ $$\lambda $$ -notation introduced by A. Church.