Lectures and tutorials

Lectures take place Monday and Wednesday. Each lecture is immediately followed by a tutorial.


118 Sep Naturals20 Sep Induction22 Sep Relations
225 Sep28 Sep
32 Oct Equality (no class, read on your own)4 Oct Isomorphism (no class, read on your own)
49 Oct Connectives11 Oct Negation & Quantifiers
516 Oct Decidable18 Oct Lambda
623 Oct Lambda & Properties25 Oct Properties
730 Oct DeBruijn1 Nov More
86 Nov Inference8 Nov Untyped
913 Nov Untyped15 Nov Eval
1020 Nov extra tutorial23 Nov extra tutorial
1127 Nov Propositions as Types29 Nov (no class)


Assessment for the course is as follows.

  • five courseworks, sixteen points each, 80%
  • optional project, take a research paper and formalise its development, 20%

In order to conform with the University’s Common Marking Scheme, students may typically get only 10 points or less (out of 20) on the optional project. Attempting the optional project may not be a good use of time compared to other courses where there are easier marks to be had.


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

  • Assignment 1 cw1 due 12 noon Thursday 5 October (Week 3)
  • Assignment 2 cw2 due 12 noon Thursday 19 October (Week 5)
  • Assignment 3 cw3 due 12 noon Thursday 2 November (Week 7)
  • Assignment 4 cw4 due 12 noon Thursday 16 November (Week 9)
  • Assignment 5 cw5 due 12 noon Thursday 23 November (Week 10) Use file Exam. Despite the rubric, do all three questions.

How to submit coursework

Go to the TSPL Learn course and select “Assessment” from the left hand menu. Select the “Assignment Submission” folder and then click on the link “submit your coursework here”. This will take you to the Gradescope interface.

For anyone who has sat an online exam, Gradescope should look familiar. Gradescope programming assignments differ from exams in that it offers three options for submitting your work:

  • Drag and drop your code file(s) into Gradescope
  • Submit a GitHub repository
  • Submit a Bitbucket repository

For the last two, you need to link your account to submit from GitHub or Bitbucket if you have not already. Instructions to do so are here.

Optional project

The optional project is to take a research paper and formalise all or part of it in Agda. In the past, some students have submitted superb optional projects that contributed to ongoing research. Talk to me about what you would like to submit.

  • Optional project cw6 due 12 noon Thursday 1 December (Week 11)

Additional reading