TSPL: Course notes (Fall 2024)
Staff
- Instructor Philip Wadler
- Teaching assistants Malin Altenmüller, Louis Lemonnier
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
Links
Schedule
| Week | Mon | Wed | Fri | |
|---|---|---|---|---|
| 4 | 8 Oct Naturals | 9 Oct Induction | 10 Oct Relations | |
| 5 | 15 Oct Equality | 16 Oct Isomorphism | 17 Oct Connectives | |
| 6 | 22 Oct Negation | 23 Oct Quantifiers | 24 Oct Decidable | |
| 7 | 29 Oct Lists | 30 Oct Lambda | 31 Oct Lambda | |
| 8 | 5 Nov Properties | 6 Nov Properties | 7 Nov DeBruijn | |
| 9 | 12 Nov More | 13 Nov More | 14 Nov Inference | |
| 10 | 19 Nov Inference | 20 Nov Untyped | 21 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
John Reynolds, Three Approaches to Type Structure, Mathematical Foundations of Software Development, LNCS 185, pages 97–138, 1985.
Henk Barendregt, Introduction to generalized type systems Journal of Functional Programming, 1(2): 125–154, 1991.
Vladimir Gapayev, Michael Levin, Benjamin Pierce. Recursive Subtyping Revealed, International Conference on Functional Programming, 2000.
Philip Wadler. Propositions as Types, Communications of the ACM, 58(12): 75–84, December 2015.