Figure 3: A program in Church's typed lambda calculus, 1940.