TSPL: Course notes
Staff
- Instructor Philip Wadler
- Teaching assistants
Lectures
Lectures take place Monday, Wednesday, and Friday in AT 7.02. (Moved from AT 5.07 and AT 4.12.)
- 9.00β9.50am Lecture
- 10.00β10.50am Tutorial
| Week | Mon | Wed | Fri |
|---|---|---|---|
| 1 | 17 Sep Naturals | 19 Sep Induction | 21 Sep Induction |
| 2 | 24 Sep Relations (Chad) | 26 Sep Relations (Chad) | 28 Sep (no class) |
| 3 | 1 Oct Equality & Isomorphism | 3 Oct Connectives | 5 Oct Negation |
| 4 | 8 Oct Quantifiers | 10 Oct Decidable | 12 Oct (tutorial only) |
| 5 | 15 Oct Lists | 17 Oct (tutorial only) | 19 Oct Lists |
| 6 | 22 Oct Lambda | 24 Oct (no class) | 26 Oct Properties |
| 7 | 29 Oct DeBruijn | 31 Oct More | 2 Nov Inference |
| 8 | 5 Nov (no class) | 7 Nov (tutorial only) | 9 Nov Untyped |
| 9 | 12 Nov (no class) | 14 Nov (tutorial only) | 16 Nov (no class) |
| 10 | 19 Nov (no class) | 21 Nov Propositions as Types | 23 Nov (no class) |
| 11 | 26 Nov (no class) | 28 Nov Quantitative (Wen) | 30 Nov (mock exam) |
Assignments
For instructions on how to set up Agda for PLFA see Getting Started.
- Assignment 1 cw1 due 4pm Thursday 4 October (Week 3)
- Assignment 2 cw2 due 4pm Thursday 18 October (Week 5)
- Assignment 3 cw3 due 4pm Thursday 1 November (Week 7)
- Assignment 4 cw4 due 4pm Thursday 15 November (Week 9)
- Assignment 5 cw5 due 4pm Thursday 22 November (Week 10)
Use file Exam. Despite the rubric, do all three questions.
Assignments are submitted by running
submit tspl cwN AssignmentN.lagda
where N is the number of the assignment.
Mock exam
Here is the text of the second mock and the exam instructions.