Link Search Menu Expand Document
Types & Lambda

COMS30040

Types and Lambda Calculus

Welcome to the home of COMS30040: Types and Lambda Calculus. This unit introduces you to type theory and the pure lambda calculus, which are two hugely influential parts of logic and the theory of programming languages.

Staff

The unit is run by Steven Ramsay (lectures), Samantha Frohlich (classes) and Eddie Jones (classes).

Steven Ramsay Samantha Frohlich Eddie Jones
Steven Sam Eddie

Technology

We will be using Microsoft Teams for all the interactive parts of the unit. You should have already been invited/forcibly-added to the COMS30040 team. Within the team you will find the following channels:

  • General: announcements appear here and all the unit teaching materials can be accessed from the tabs.
  • Discussion Board: post your questions here and we will try to answer them asap.
  • QA Session: the lecturer Q&A sessions are held here and, afterwards, the recordings will be linked from the channel conversation.
  • Room E: Eddie’s classes are held here and your work will be returned to you through the Files tab.
  • Room S: Sam’s classes are held here and your work will be returned to you through the Files tab.

To attend a QA session or a class, just goto the appropriate channel in Teams and wait for a post that says that this week’s meeting has started, this post will have a “Join” button that you can click to come in.

Workload

This is a 10 credit unit, and the unit runs during weeks 1–7. You should expect to spend around 10 hours per week working on it. There are 5 main activities:

  • Prerecorded lectures. At the start of each week, three prerecorded lectures will be posted on the unit website which you need to watch in your own time.
  • Problems. You will only learn on this unit by completing the problem sheets and exercises. There is one sheet released each week and you are expected to work on it in your own time.
  • Online classes. Excepting week 1, every Tuesday there is a problem class in which our senior TAs, Eddie Jones and Samantha Frohlich, will guide you through the solutions and try to help with any questions you have. Note: Monday 5pm-6pm is timetabled for “Peer Learning”, we will not be using this slot.
  • Lecturer Q&A. Excepting week 1, every Monday at 3pm there will be a one-hour Q&A with the lecturer. In week 1, this will start at 3:30pm due to Welcome Week events. Apart from week 1, I recommend you attend the Q&A only if you wish to ask a question (it will be recorded so you will not miss out on an answer).
  • Reading/Revising. You will often benefit from alternative explanations of the same concepts, which would not fit into the time available for lectures. You will need to spend time revising and rethinking topics before you can solve the associated problems.

Each week, I recommend that you adopt the following pattern:

  • Weeks 1 and 2: Watch the first core lecture and the supplementary lecture and attend your problem class (in any order). Then attempt this week’s problem sheet and be sure to submit your solutions before Thursday 5pm. Finally watch the second core lecture. If anything is unclear, come to the Q&A at the start of the following week and let’s discuss it.
  • Weeks 3 to 7: Watch the first core lecture and attend your problem class (in any order). Then attempt this week’s problem sheet and be sure to submit your solutions before Thursday 5pm. Finally watch the second core lecture and the supplementary lecture. If anything is unclear, come to the Q&A at the start of the following week and let’s discuss it.

Assessment

This unit is assessed by a written exam in the January assessment period and again in the August/September assessment period. The date of the former is 20 January at 09:45 GMT, the date of the latter will be announced with the exam timetabling on August 3rd. Both exams follow the same format, described below.

The exam consists of two questions of 25 marks each, and each question is the same format as a (short) problem sheet. One question is on the untyped lambda calculus and the other on the type system. You may use the lecture notes, but you must not collaborate.

Shortly before the exam, a Blackboard assessment point will be created on the Blackboard page for this unit. At the time of the exam you should navigate to this assessment point where you will be able to download a copy of the paper in PDF format. You may start the exam immediately. You will have two hours to write your solutions and a further period of additional time (which is yet to be standardised across the department) in which to upload your solutions back to the assessment point (e.g. after scanning or photographing them). See here for the University’s guidance on uploading handwritten materials.

The questions are set so that, roughly two eighths are of 1* difficulty (routine calculations), five eighths are of 2* difficulty (problems that require thought but which follow a familiar pattern) and the remaining one eighth is of 3* difficulty (problems which are unusual and/or very difficult). The last 3 or 4 marks of each question is that of 3* difficulty, so you may wish to leave these parts to the end. You can solve the problems in any order as long as you indicate clearly.

The following are (adaptations) of past papers:

The first questions of these past papers were about recalling a definition. There will be no questions of this form on the exam this year because you are able to use the lecture notes.