Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.
Sign up to join this community
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")
In the very next paragraph of that book (see HoTT, p. 2) they give an informal characterization of what qualifies a language system (or logic) as a type system, namely that: in it all terms are typed.
By "Church's type system" they're referring to the simply typed lambda calculus (introduced in 1940).
In 1930s, in particular while preparing his negative solution to the decision problem, Church had introduced a system of untyped lambda calculus. This, of course, was not a type theory.
The 1940 system, however, is a type theory, because in it all terms are typed (see, for example (T&S), Section 1.2 for how exactly this is done). By "lambda-calculus as a type system" they're referring to this second, simply typed version of lambda calculus.
(T&S) Troelstra, A.S. & Schwichtenberg, H. Basic Proof Theory, 1996.
