---
title     : "TSPL: Course notes"
layout    : page
permalink : /TSPL/
---

## Staff

* **Instructor**
    [Philip Wadler](https://homepages.inf.ed.ac.uk/wadler)
* **Teaching assistants**
  - [Wen Kokke](mailto:wen.kokke@ed.ac.uk)
  - [Chad Nester](mailto:chad.nester@gmail.com)

## 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

<table>
 <tr>
  <th>Week</th>
  <th>Mon</th>
  <th>Wed</th>
  <th>Fri</th>
 </tr>
 <tr>
  <td>1</td>
  <td><b>17 Sep</b> <a href="/Naturals/">Naturals</a></td>
  <td><b>19 Sep</b> <a href="/Induction/">Induction</a></td>
  <td><b>21 Sep</b> <a href="/Induction/">Induction</a></td>
 </tr>
 <tr>
  <td>2</td>
  <td><b>24 Sep</b> <a href="/Relations/">Relations</a> (Chad)</td>
  <td><b>26 Sep</b> <a href="/Relations/">Relations</a> (Chad)</td>
  <td><b>28 Sep</b> (no class)</td>
 </tr>
 <tr>
  <td>3</td>
  <td><b>1 Oct</b> <a href="/Equality/">Equality</a> &amp; <a href="/Isomorphism/">Isomorphism</a></td>
  <td><b>3 Oct</b> <a href="/Connectives/">Connectives</a></td>
  <td><b>5 Oct</b> <a href="/Negation/">Negation</a></td>
 </tr>
 <tr>
  <td>4</td>
  <td><b>8 Oct</b> <a href="/Quantifiers/">Quantifiers</a></td>
  <td><b>10 Oct</b> <a href="/Decidable/">Decidable</a></td>
  <td><b>12 Oct</b> (tutorial only)</td>
 </tr>
 <tr>
  <td>5</td>
  <td><b>15 Oct</b> <a href="/Lists/">Lists</a></td>
  <td><b>17 Oct</b> (tutorial only)</td>
  <td><b>19 Oct</b> <a href="/Lists/">Lists</a></td>
 </tr>
 <tr>
  <td>6</td>
  <td><b>22 Oct</b> <a href="/Lambda/">Lambda</a></td>
  <td><b>24 Oct</b> (no class)</td>
  <td><b>26 Oct</b> <a href="/Properties/">Properties</a></td>
 </tr>
 <tr>
  <td>7</td>
  <td><b>29 Oct</b> <a href="/DeBruijn/">DeBruijn</a></td>
  <td><b>31 Oct</b> <a href="/More/">More</a></td>
  <td><b>2 Nov</b> <a href="/Inference/">Inference</a></td>
 </tr>
 <tr>
  <td>8</td>
  <td><b>5 Nov</b> (no class)</td>
  <td><b>7 Nov</b> (tutorial only)</td>
  <td><b>9 Nov</b> <a href="/Untyped/">Untyped</a></td>
 </tr>
 <tr>
  <td>9</td>
  <td><b>12 Nov</b> (no class)</td>
  <td><b>14 Nov</b> (tutorial only)</td>
  <td><b>16 Nov</b> (no class)</td>
 </tr>
 <tr>
  <td>10</td>
  <td><b>19 Nov</b> (no class)</td>
  <td><b>21 Nov</b> Propositions as Types</td>
  <td><b>23 Nov</b> (no class)</td>
 </tr>
 <tr>
  <td>11</td>
  <td><b>26 Nov</b> (no class)</td>
  <td><b>28 Nov</b> Quantitative (Wen)</td>
  <td><b>30 Nov</b> (mock exam)</td>
 </tr>
</table>

## Assignments

For instructions on how to set up Agda for PLFA see [Getting Started](/GettingStarted/).

* [Assignment 1][Assignment1] cw1 due 4pm Thursday 4 October (Week 3)
* [Assignment 2][Assignment2] cw2 due 4pm Thursday 18 October (Week 5)
* [Assignment 3][Assignment3] cw3 due 4pm Thursday 1 November (Week 7)
* [Assignment 4][Assignment4] cw4 due 4pm Thursday 15 November (Week 9)
* [Assignment 5](/tspl/first-mock.pdf) cw5 due 4pm Thursday 22 November (Week 10)
  <br />
  Use file [Exam][Exam]. Despite the rubric, do **all three questions**.
  

Assignments are submitted by running
``` bash
submit tspl cwN AssignmentN.lagda
```
where N is the number of the assignment.

## Mock exam

Here is the text of the [second mock](/tspl/second-mock.pdf)
and the exam [instructions](/tspl/instructions.pdf).
