Staff

Lectures and tutorials

Lectures take place Monday and Thursday. Monday’s lecture is immediately followed by a tutorial.

  • 10.00–12.00 Monday Lecture and Tutorial George Square 50, room G.02 (50GS G.02).
  • 10.00–10.50 Thursday Lecture Lister Learning and Teaching Centre, room G.13 (LLTC G.13).
WeekMonThu
119 Sep (Bank Holiday)22 Sep Naturals
226 Sep Induction29 Sep Relations
33 Oct Equality & Isomorphism6 Oct Connectives
410 Oct Negation13 Oct Quantifiers
517 Oct Decidable & Lists20 Oct Lambda
624 Oct Lambda27 Oct Properties
731 Oct DeBruijn3 Nov More
87 Nov Inference10 Nov Untyped
914 Nov Blame and Coercions17 Nov
1021 Nov24 Nov
1128 Nov Propositions as Types1 Dec 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 12 noon Thursday 6 October (Week 3)
  • Assignment 2 cw2 due 12 noon Thursday 20 October (Week 5)
  • Assignment 3 cw3 due 12 noon Thursday 3 November(Week 7)
  • Assignment 4 cw4 due 12 noon Thursday 17 November (Week 9)
  • Assignment 5 cw5 due 12 noon Thursday 24 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. In the past, some students have submitted superb optional projects that contributed to ongoing research. One possible paper to tackle is here. Talk to me if you want to formalise something else.

  • Optional project cw6 due 12 noon Thursday 28 November (Week 11)

Submit the optional project by running

submit tspl essay Essay.lagda.md

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