Friday’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. This lecture presented the simply-typed lambda-calculus and some examples of programming language support for first-class functions.
Link: Slides for Lecture 2
Homework
Read this paper and do some of the exercises.
- Achim Jung. A Short Introduction to the Lambda-Calculus.
You may find it helpful to first read pages 1–7 of Pierce’s
Foundational Calculi for Programming Languages which introduces the untyped lambda-calculus.
Other Reading
 |
Alligator Eggs! A Puzzle Game Bret Victor 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 2016-09-23 |
 |
A Set of Postulates for the Foundation of Logic Alonzo Church Annals of Mathematics Series 2, 33:346–366. Princeton, 1932. The original lambda-calculus. |
 |
Types and Programming Languages Benjamin C. Pierce MIT Press, 2002 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 Benjamin C. Pierce, Editor Builds on the previous book with chapters presenting several concrete applications of types to programming, each by experts in the field. Links: Author’s page; Publisher’s page; Edinburgh University Library copies |