Welcome
Welcome to the home of COMS30040: Types and Lambda Calculus. This unit introduces you to the mathematical foundations of programming languages, with an emphasis on functional programs and type systems.
Our focus will be on the expressive power of the language with and without types; the algorithmics of assigning types to terms; and the close correspondence with logic and proof. A secondary goal is to teach you to write mathematical proofs.
This unit prepares you for COMSM0067: Advanced Topics in Programming Languages in the programming languages theme in your fourth year, but is not a prerequesite. It shares themes and techniques with the unit MATH30100: Logic.
Contacts
The unit is run by Steven Ramsay (lectures) and Tom Divers and Piotr Kozicki (classes).
Outside of lectures and classes, if you have any questions about the material, the way the unit runs or are just curious about programming language theory or logic more generally, then please post to the General channel of the Team. We would like to hear from you!
Schedule
You should expect to spend around 6-7 hours per week working on this unit.
-
Lectures (2 hr). Excepting Week 1 (which has an additional Friday lecture), There are two lectures per week, given on campus:
- Monday at 2pm in FRY G.09
- Wednesday at 10am in FRY G.09
Each lecture corresponds to one chapter in the lecture notes.
-
Problem Sheets (3 hr). You will only learn by completing the problem sheets. There is one sheet released each week. You should aim to spend at least two hours working on each problem sheet each week, in your own time. You will need to consult the course lecture notes whilst attempting the problems. You should complete the Week n problem sheet and submit it no later than the end of the (following) Monday of Week (n+1).
Attempting the problem sheets each week is the single most important thing to do in this unit. One can certainly excel without attending a single lecture, but not doing the problems will lead to certain disaster.
-
Problem Class (1 hr). You should attend a problem class each week to discuss the answers to the problems of the previous week and look ahead to problems of the next week. There will be no class in Week 1, since you have not yet had time to complete a problem sheet.
- Group 1: Friday 11am in Queens 1.58
- Group 2: Friday 11am in Queens 1.68
- Office Hours (0-1 hr). Starting in week 2, Steven will be running office hours every Thursday from 11am-12noon in his office, MVB 2.46.