Alonzo Church
Respondió al problema de decisión de Hilbert unos meses antes que Turing, con una herramienta que resultó ser el antepasado de los lenguajes de programación.
Church era matemático en Princeton y desarrolló el cálculo lambda a principios de los años treinta: un sistema formal en el que todo es una función y calcular consiste en reescribir expresiones. En la primavera de 1936 lo usó para demostrar que el Entscheidungsproblem no tiene solución. Turing llegó a la misma respuesta ese mismo año con un modelo completamente distinto, después fue su doctorando entre 1936 y 1938, y ambos sistemas resultaron computar exactamente las mismas cosas — lo que hoy llamamos la tesis de Church-Turing.
El cálculo lambda no se quedó dentro de la demostración. Su variante con tipos simples de 1940 es el antepasado de todo sistema de tipos posterior, y LISP, ML, Haskell y las expresiones lambda que desde entonces se han colado en C++, Java y Python descienden directamente de la notación de Church para las funciones anónimas.
Su lista de discípulos quizá sea su mayor huella: Turing, Kleene, Rosser, Dana Scott, Michael Rabin, Raymond Smullyan. Church era meticuloso hasta un punto que se volvió anécdota — lavaba la pizarra antes de escribir en ella, incluso cuando ya estaba limpia — y fundó en 1936 el Journal of Symbolic Logic, que después mantuvo en orden durante cuatro décadas.