TSPL: Course notes
- Instructor Philip Wadler
- Teaching assistants
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
|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)|
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.
Here is the text of the second mock and the exam instructions.