Introduction To Lambda Calculus

This course offers an introductory overview of lambda calculus, which serves as the basis for various functional programming languages such as Haskell. In the initial two weeks, we focus on fundamental concepts like function representation, function abstraction and application, and term reduction (i.e., computation). A particular emphasis is placed on the creation of complex functions and data structures from the ground up, a topic often overlooked in most textbooks and online resources. The following two weeks will address simply typed lambda calculus. We will establish a formal system that allows us to logically deduce that a term M possesses a type $\tau$. An algorithm for assigning principal types to typable terms will be demonstrated through examples. Lastly, we will briefly explore the idea of the relationship between types as logical formulas and the proofs of these logical formulas as type deductions of lambda terms.