# lambda calculus as a type theory

From the Introduction section of Homotopy Type Theory book:

Type theory was originally invented by Bertrand Russell ... It was later developed as a rigorous formal system in its own right(under tha name "$\lambda$-calculus").

Can anyone explain me this sentence? I'm having trouble seeing $\lambda$-calculus as a type system.

(also in the same paragraph, $\lambda$-calculus called as "Church's type system")

• While it may not seem obvious, the book "Types and Programming Languages" by Benjamin C. Pierce explains this in detail by going from lambda calculus up to a simple typed programming language. See: cs.stackexchange.com/q/9548/268 – Guy Coder Aug 12 '13 at 10:11