Simply Typed Lambda Calculus: Foundations and Properties

This lecture introduces the simply typed lambda calculus (STLC), focusing on its syntax, semantics, and type system. The instructor begins by discussing the fundamental concepts of lambda calculus, including functional abstraction, substitution, and reduction. The lecture emphasizes the importance of type systems in programming languages, outlining the properties expected from them, such as progress and preservation. The instructor defines the syntax of STLC, incorporating variables, constants, and function applications. The semantics is then established, detailing how expressions can be evaluated and reduced. The lecture also covers the inductive definitions of typing rules, demonstrating how to determine whether expressions are well-typed. The instructor illustrates the significance of these rules through examples, highlighting the challenges posed by bound variables and substitutions. Finally, the lecture concludes with a discussion on the soundness of the type system, proving that well-typed programs either evaluate to values or can make progress, ensuring that they do not become stuck in non-terminating states.