Lecture 6: The Simply Typed Lambda-Calculus

In today's class, we show that SML is not an adequate specification language for higher-order encodings, but that the simply typed lambda-calculus is. We give a formal definition of this calculus, define canonical forms, and define what it means for a representation function to be adequate.

Suggested Reading Materials:

Frank Pfenning. Computation and Deduction, Chapter 3

Previous lecture: Lecture 5
Next lecture: Lecture 7