Staff

Lectures and tutorials

Lectures take place Tuesday, Wednesday, and Thursday weeks 4–10. Lectures on Tuesday and Thursday are immediately followed by a tutorial.

  • 12.10–14.00 Tuesday Lecture and Tutorial Teaching Room 13 (01M.473) - Doorway 3 - Medical School, Teviot
  • 12.10–13.00 Wednesday Lecture G.07 Meadows Lecture Theatre - Doorway 4 - Medical School, Teviot
  • 12.10–14.00 Thursday Lecture and Tutorial 5.3 - Lister Learning and Teaching Centre

Course textbook

Schedule

WeekMonWedFri
48 Oct Naturals9 Oct Induction10 Oct Relations
515 Oct Equality16 Oct Isomorphism17 Oct Connectives
622 Oct Negation23 Oct Quantifiers24 Oct Decidable
729 Oct Lists30 Oct Lambda31 Oct Lambda
85 Nov Properties6 Nov Properties7 Nov DeBruijn
912 Nov More13 Nov More14 Nov Inference
1019 Nov Inference20 Nov Untyped21 Nov Propositions as Types

Assessment

Assessment for the course is as follows.

  • four courseworks, marked best three out of four, 80%
  • essay, take a research paper and formalise its development, 20%

Because there is no final, we need to be able to check that students can explain their work during tutorials. For this reason, you can only achieve marks on coursework if you have attended at least one of the four tutorial sessions in the week before it is due.

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 essay. Attempting the essay may not be a good use of time compared to other courses where there are easier marks to be had. Not all students are expected to attempt the essay.

Coursework

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

  • Assignment 1 cw1 due 12 noon Friday 18 October (Week 5)
  • Assignment 2 cw2 due 12 noon Friday 1 November (Week 7)
  • Assignment 3 cw3 due 12 noon Friday 15 November (Week 9)
  • Assignment 4 cw4 due 12 noon Friday 29 November (Week 11)
  • Essay cw5 due 12 noon Thursday 23 January 2025 (Week 2, Semester 2)

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.

Essay

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

Additional reading