Lecture 2: Terms and Types
Today’s lecture introduced the first topic for the course, on types in programming languages: some of the ways they are used, and their relation to the mathematical models of lambdacalculus and type theory. Students identified a range of languages that use types, with some variation across what they are used for and how they are implemented. The lecture introduced the simplytyped lambdacalculus: its terms and types with αconversion and βreduction. The next lecture will start with some examples of programming language support for firstclass functions.
Link: Slides for Lecture 2; Recording of Lecture 2
Homework
1. Watch This
MIT Technology Review: 35 Innovators under 35 Jean Yang Links: Video (2’18”); Prof. Yang at CMU 
2. Do This

Find out what the Blub Paradox is.

Read the article that named it
3. Read This
Read this paper and do some of the exercises.

Achim Jung. A Short Introduction to the LambdaCalculus.
You may find it helpful to also read pages 1–7 of Pierce’s Foundational Calculi for Programming Languages which introduces the untyped lambdacalculus.
Other Reading
The first of these is secretly about lambdacalculus terms and their execution. The second is much less colourful but is useful background reading.
Alligator Eggs! Links: Alligator Eggs; Animation 

FirstClass Function Wikipedia I think this a fair overview, leading in to issues of anonymous functions, closures, and higherorder functions in programming languages. Links: Wikipedia page now; Wikipedia page as at 20180920 
References
A Set of Postulates for the Foundation of Logic The original lambdacalculus. 

Types and Programming Languages A comprehensive introduction to type systems in computer science and programming languages. Links: Author’s page; Publisher’s page; Edinburgh University Library copies 

Advanced Topics in Types and Programming Languages Builds on the previous book with chapters presenting several concrete applications of types to programming, each written by experts in the field. Links: Author’s page; Publisher’s page; Edinburgh University Library copies 