Comment by cubefox

"Lambda calculus" is sometimes used to mean "simply typed lambda calculus", which is mainly used to refer to simple type theory (STT), which is also called "Church's type theory". STT is also often identified with higher-order logic, since just two primitive types (basic "entities" like chairs and the "truth values" T/F) and the function type (a --> b) suffice to express arbitrary logical objects. STT is indeed an invention of Church, and it has had a major influence on other modern type theories, which are often described as extensions of simple type theory. These also influenced some programming languages with complex type system, like Haskell.