---
title : "TSPL: Course notes"
permalink : /TSPL/2019/
---
## Staff
* **Instructor**
[Philip Wadler](https://homepages.inf.ed.ac.uk/wadler)
* **Teaching assistants**
- [Wen Kokke](mailto:wen.kokke@ed.ac.uk)
- [Orestis Melkonian](mailto:o.melkonian@sms.ed.ac.uk)
## Lectures
Lectures take place Monday, Wednesday, and Friday in AT 5.07.
* **10.00--10.50am** Lecture
* **11.10--12.00noon** Tutorial
<table>
<thead>
<tr>
<th scope="col">Week</th>
<th scope="col">Mon</th>
<th scope="col">Wed</th>
<th scope="col">Fri</th>
</tr>
</thead>
<tbody>
<tr>
<td>1</td>
<td><b>16 Sep</b> <a href="/Naturals/">Naturals</a></td>
<td><b>18 Sep</b> <a href="/Induction/">Induction</a></td>
<td><b>20 Sep</b> <a href="/Relations/">Relations</a></td>
</tr>
<tr>
<td>2</td>
<td><b>23 Sep</b> (no class)</td>
<td><b>25 Sep</b> (tutorial only)</td>
<td><b>27 Sep</b> (no class)</td>
</tr>
<tr>
<td>3</td>
<td><b>30 Sep</b> <a href="/Equality/">Equality</a> &
<a href="/Isomorphism/">Isomorphism</a></td>
<td><b>2 Oct</b> <a href="/Connectives/">Connectives</a></td>
<td><b>4 Oct</b> <a href="/Negation/">Negation</a></td>
</tr>
<tr>
<td>4</td>
<td><b>7 Oct</b> <a href="/Quantifiers/">Quantifiers</a></td>
<td><b>9 Oct</b> <a href="/Decidable/">Decidable</a></td>
<td><b>11 Oct</b> (tutorial only, 10.00–10.50)</td>
</tr>
<tr>
<td>5</td>
<td><b>14 Oct</b> <a href="/Lists/">Lists</a></td>
<td><b>16 Oct</b> <a href="/Lambda/">Lambda</a></td>
<td><b>18 Oct</b> <a href="/Lambda/">Lambda</a> and
<a href="/Properties/">Properties</a></td>
</tr>
<tr>
<td>6</td>
<td><b>21 Oct</b> <a href="/Properties/">Properties</a></td>
<td><b>23 Oct</b> <a href="/DeBruijn/">DeBruijn</a></td>
<td><b>25 Oct</b> <a href="/More/">More</a></td>
</tr>
<tr>
<td>7</td>
<td><b>28 Oct</b> <a href="/Inference/">Inference</a></td>
<td><b>30 Oct</b> <a href="/Untyped/">Untyped</a></td>
<td><b>1 Nov</b> (no class) </td>
</tr>
<tr>
<td>8</td>
<td><b>4 Nov</b> (no class) </td>
<td><b>6 Nov</b> Blame and Coercions </td>
<td><b>8 Nov</b> (no class) </td>
</tr>
<tr>
<td>9</td>
<td><b>11 Nov</b> (no class) </td>
<td><b>13 Nov</b> Additional Reading </td>
<td><b>15 Nov</b> (no class) </td>
</tr>
<tr>
<td>10</td>
<td><b>18 Nov</b> (no class) </td>
<td><b>20 Nov</b> Propositions as Types </td>
<td><b>22 Nov</b> (no class) </td>
</tr>
<tr>
<td>11</td>
<td><b>25 Nov</b> Quantitative (Wen) </td>
<td><b>27 Nov</b> (no class) </td>
<td><b>29 Nov</b> Mock Exam </td>
</tr>
</tbody>
</table>
## Assessment
Assessment for the course is as follows.
* five courseworks, five points each, including a take-home mock exam
(the "mock mock"), <b>25%</b>
* optional project, take a research paper and formalise its development, <b>25%</b>
* mock exam, online with Agda proof assistant under exam conditions, <b>0%</b>
* final exam, online with Agda proof assistant, <b>50%</b>
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](/GettingStarted/).
* [Assignment 1](/TSPL/2019/Assignment1/) cw1 due 4pm Thursday 3 October (Week 3)
* [Assignment 2](/TSPL/2019/Assignment2/) cw2 due 4pm Thursday 17 October (Week 5)
* [Assignment 3](/TSPL/2019/Assignment3/) cw3 due 4pm Thursday 31 October (Week 7)
* [Assignment 4](/TSPL/2019/Assignment4/) cw4 due 4pm Thursday 14 November (Week 9)
* [Assignment 5](/TSPL/2019/Mock1.pdf) cw5 due 4pm Thursday 21 November (Week 10)
Use file [Exam](/TSPL/2019/Exam/). Despite the rubric, do **all three questions**.
Assignments are submitted by running
``` bash
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. I suggest formalising the paper
[here](https://homepages.inf.ed.ac.uk/wadler/topics/blame.html#coercions),
but talk to me if you want to formalise something else.
(A more recent draft of the same paper is
[here](https://homepages.inf.ed.ac.uk/wadler/papers/coercions-jfp/coercions-jfp.pdf).)
* Optional project cw6 due 4pm Thursday 28 November (Week 11)
Submit the optional project by running
``` bash
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
* John Reynolds,
[Three Approaches to Type Structure][reynolds],
_Mathematical Foundations of Software Development_,
LNCS 185, pages 97–138, 1985.
* Henk Barendregt,
[Introduction to generalized type systems][barendregt]
_Journal of Functional Programming_, 1(2): 125–154, 1991.
* Vladimir Gapayev, Michael Levin, Benjamin Pierce.
[Recursive Subtyping Revealed][gapayev],
_International Conference on Functional Programming_, 2000.
[reynolds]: https://homepages.inf.ed.ac.uk/wadler/papers/reynolds/three-approaches.pdf
[barendregt]: https://homepages.inf.ed.ac.uk/wadler/papers/barendregt/pure-type-systems.pdf
[gapayev]: https://homepages.inf.ed.ac.uk/wadler/papers/gapayev/gapayev-et-al-icfp2000.pdf