Alonzo Church publicó en 1936 el cálculo lambda, un sistema formal para expresar cómputo mediante funciones y su aplicación. Introduce la noción de función como ciudadano de primer orden y de abstracción funcional, demostrando que existen problemas no computables (independientemente y de forma simultánea a Turing). Es el fundamento teórico de toda la programación funcional: ML, Haskell, OCaml y Lisp derivan directamente de este formalismo.