Amir Goharshady - Lambda Calculus and Types

↢ Back to the List of Courses

Lambda Calculus and Types

Hilary Term 2025

Number of Students: 56

Average Rating by the Students: 4.74/5.0

Course Textbook

Andrew Ker has prepared excellent textbook-quality lecture notes for this course and we will use them.

Andrew Ker's Lecture Notes

Previous Offering

Last year, Lambda Calculus and Types was taught by Bartek Klin and its course material is available here. I will also use his slides in many of the lectures.

Problem Sheets

Problems are chosen from Andrew Ker's Lecture Notes above.

Problem Sheet 1: Exercises 1.1, 1.2 (first part), 1.5, 1.6, 1.8, 1.10
Problem Sheet 2: Exercises 2.1, 2.2, 2.5, 2.9 (Can you define the normal terms using trees?), 2.11, 2.12
Problem Sheet 3: Exercises 3.1, 3.2, 3.5, 3.6, 3.7 (using 3.5 (ii)), 4.2
Problem Sheet 4: Exercises 4.1, 4.2, 4.4, 4.8, 4.9, 4.10
Problem Sheet 5: Exercises 5.1 - 5.4
Problem Sheet 6: Exercises 6.1, 6.2, 6.3, 6.4, 6.5, 6.8, 6.9
Problem Sheet 7: Exercises 7.1, 7.3, 7.4, 7.5, 7.6

Lecture 1: Introduction to Lambda Calculus and its Syntax

Lambda Calculus and Types

Course Textbook

Previous Offering

Problem Sheets

Lecture 1: Introduction to Lambda Calculus and its Syntax

Lecture 2: Alpha and Beta Conversion

Lecture 3: First Recursion Theorem

Lecture 4: Church-Rosser Reductions

Lecture 5: Uniqueness of Normal Forms

Lecture 6: Böhm's Theorem and Reduction Strategies

Lecture 7: Leftmost Reductions, Booleans and Church Numerals

Lecture 8: Solvability, Definability and Church-Kleene

Lecture 9: Undecidability, Halting, Rice and Scott-Curry

Lecture 10: Combinatory Logic

Lecture 11: Lambda-algebras and Simple Types

Lecture 12: Simple Types and Weak Normalisation

Lecture 13: Strong Normalisation

Lecture 14: Principal Types

Lecture 15: System T and Curry-Howard

Lecture 16: Gödel's Incompleteness Theorem