 The correspondence to be descried here between logic and the \(\lambda\)-calculus is seen with the help of an apparatus known as types. This section sketches the beginnings of the development of the subject known as type theory. We are interested in developing type theory only so far as to make the so-called Curry-Howard-de Bruijn correspondence visible. A more detailed treatment can be found in the entry on  type theory;  see also (Hindley, 1997) and (Barendregt, Dekkers, Statman, 2013).