In computer science, especially in the field of programming languages, when we’re trying to understand or prove facts about computation, we use a tool called λ (“lambda”) calculus.

λ calculus was designed by an American mathematician named Alonzo Church (1903--1995)
as part of one of the first proofs of the Halting problem (which we’ll talk more about in 27, *The Halting Problem*).
Turing is largely credited as the person who solved that,
and his proof is the one that most people remember.
But Church did it independently of Turing, and his proof was actually published first!

λ calculus is probably the most widely used theoretical tool in computer science. For example, among programming-language ...

Start Free Trial

No credit card required