Alonzo Church published in 1936 the lambda calculus, a formal system for expressing computation via functions and their application. He introduces functions as first-class citizens and functional abstraction, showing non-computable problems exist (independently and simultaneously with Turing). It is the theoretical foundation of all functional programming: ML, Haskell, OCaml, and Lisp derive directly from this formalism.