Lectures take place Monday, Wednesday, and Friday in AT 7.02. (Moved from AT 5.07 and AT 4.12.)

  • 9.00–9.50am Lecture
  • 10.00–10.50am Tutorial
117 Sep Naturals19 Sep Induction21 Sep Induction
224 Sep Relations (Chad)26 Sep Relations (Chad)28 Sep (no class)
31 Oct Equality & Isomorphism3 Oct Connectives5 Oct Negation
48 Oct Quantifiers10 Oct Decidable12 Oct (tutorial only)
515 Oct Lists17 Oct (tutorial only)19 Oct Lists
622 Oct Lambda24 Oct (no class)26 Oct Properties
729 Oct DeBruijn31 Oct More2 Nov Inference
85 Nov (no class)7 Nov (tutorial only)9 Nov Untyped
912 Nov (no class)14 Nov (tutorial only)16 Nov (no class)
1019 Nov (no class)21 Nov Propositions as Types23 Nov (no class)
1126 Nov (no class)28 Nov Quantitative (Wen)30 Nov (mock exam)


For instructions on how to set up Agda for PLFA see Getting Started.

  • Assignment 1 cw1 due 4pm Thursday 4 October (Week 3)
  • Assignment 2 cw2 due 4pm Thursday 18 October (Week 5)
  • Assignment 3 cw3 due 4pm Thursday 1 November (Week 7)
  • Assignment 4 cw4 due 4pm Thursday 15 November (Week 9)
  • Assignment 5 cw5 due 4pm Thursday 22 November (Week 10)
    Use file Exam. Despite the rubric, do all three questions.

Assignments are submitted by running

submit tspl cwN AssignmentN.lagda

where N is the number of the assignment.

Mock exam

Here is the text of the second mock and the exam instructions.