Staff

Lectures

Lectures take place Monday, Wednesday, and Friday in AT 5.07.

  • 10.00–10.50am Lecture
  • 11.10–12.00noon Tutorial
Week Mon Wed Fri
1 16 Sep Naturals 18 Sep Induction 20 Sep Relations
2 23 Sep (no class) 25 Sep (tutorial only) 27 Sep (no class)
3 30 Sep Equality & Isomorphism 2 Oct Connectives 4 Oct Negation
4 7 Oct Quantifiers 9 Oct Decidable 11 Oct (tutorial only, 10.00–10.50)
5 14 Oct Lists 16 Oct Lambda 18 Oct Lambda and Properties
6 21 Oct Properties 23 Oct DeBruijn 25 Oct More
7 28 Oct Inference 30 Oct Untyped 1 Nov (no class)
8 4 Nov (no class) 6 Nov Blame and Coercions 8 Nov (no class)
9 11 Nov (no class) 13 Nov Additional Reading 15 Nov (no class)
10 18 Nov (no class) 20 Nov Propositions as Types 22 Nov (no class)
11 25 Nov Quantitative (Wen) 27 Nov (no class) 29 Nov Mock Exam

Assessment

Assessment for the course is as follows.

  • five courseworks, five points each, including a take-home mock exam (the “mock mock”), 25%
  • optional project, take a research paper and formalise its development, 25%
  • mock exam, online with Agda proof assistant under exam conditions, 0%
  • final exam, online with Agda proof assistant, 50%

Students are expected to get 3–5 points each (out of 5) on the courseworks. Students who undertake the coursework and mock exam typically get 50 points (out of 50) on the final exam. In order to conform with the University’s Common Marking Scheme, students may typically get only 10 points (out of 25) 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.

Coursework

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

  • Assignment 1 cw1 due 4pm Thursday 3 October (Week 3)
  • Assignment 2 cw2 due 4pm Thursday 17 October (Week 5)
  • Assignment 3 cw3 due 4pm Thursday 31 October (Week 7)
  • Assignment 4 cw4 due 4pm Thursday 14 November (Week 9)
  • Assignment 5 cw5 due 4pm Thursday 21 November (Week 10)

Assignments are submitted by running

submit tspl cwN AssignmentN.lagda.md

where N is the number of the assignment.

Optional project

The optional project is to take a research paper and formalise all or part of it in Agda. I suggest formalising the paper here, but talk to me if you want to formalise something else. (A more recent draft of the same paper is here.)

  • Optional project cw6 due 4pm Thursday 28 November (Week 11)

Mock exam

10am-12noon Friday 29 November, AT 5.05 West Lab. An online examination with the Agda proof assistant, under DICE to let you practice for the exam and familiarise yourself with exam conditions.

Additional reading