Alonzo Church

Alonzo Church was an American mathematician and logician who developed lambda calculus in the 1930s, a formal system for expressing computation and function definition using only variable binding and substitution, which became one of the foundational formal models of what it means for a function to be computable. Church used this system to help formulate what is now known as the Church-Turing thesis, developed alongside related independent work by his student Alan Turing on the Turing machine, the widely accepted claim that any function that can be computed by an intuitively effective procedure can be computed by these formal models, a foundational statement that helped define the theoretical limits of computation itself. Church also proved that there is no general algorithm that can determine, for every possible statement in a certain class of formal logic, whether that statement is true, a result now called Church's theorem that established fundamental limits on what formal logical systems can achieve. Lambda calculus, largely a topic of interest mainly to logicians during Church's own lifetime, later became directly foundational to the design of functional programming languages and to the theoretical study of programming language semantics within computer science.