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 lambda-calculus 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 simply-typed lambda-calculus: its terms and types with α-conversion and β-reduction. The next lecture will start with some examples of programming language support for first-class 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 Lambda-Calculus.
You may find it helpful to also read pages 1–7 of Pierce’s Foundational Calculi for Programming Languages which introduces the untyped lambda-calculus.
Other Reading
The first of these is secretly about lambda-calculus terms and their execution. The second is much less colourful but is useful background reading.
Alligator Eggs! Links: Alligator Eggs; Animation |
![]() |
First-Class Function Wikipedia I think this a fair overview, leading in to issues of anonymous functions, closures, and higher-order functions in programming languages. Links: Wikipedia page now; Wikipedia page as at 2018-09-20 |
![]() |
A Set of Postulates for the Foundation of Logic The original lambda-calculus. |
![]() |
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 |
![]() |
- Lecture 1: What’s So Important About Language?
- Lecture 3: Parameterized Types and Polymorphism