Staff

Lectures

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
Week Mon Wed Fri
1 17 Sep Naturals 19 Sep Induction 21 Sep Induction
2 24 Sep Relations (Chad) 26 Sep Relations (Chad) 28 Sep (no class)
3 1 Oct Equality & Isomorphism 3 Oct Connectives 5 Oct Negation
4 8 Oct Quantifiers 10 Oct Decidable 12 Oct (tutorial only)
5 15 Oct Lists 17 Oct (tutorial only) 19 Oct Lists
6 22 Oct Lambda 24 Oct (no class) 26 Oct Properties
7 29 Oct DeBruijn 31 Oct More 2 Nov Inference
8 5 Nov (no class) 7 Nov (tutorial only) 9 Nov Untyped
9 12 Nov (no class) 14 Nov (tutorial only) 16 Nov (no class)
10 19 Nov (no class) 21 Nov Propositions as Types 23 Nov (no class)
11 26 Nov (no class) 28 Nov Quantitative (Wen) 30 Nov (mock exam)

Assignments

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.