diff --git a/Makefile b/Makefile
index 991d38c1..9f7b534f 100644
--- a/Makefile
+++ b/Makefile
@@ -1,4 +1,4 @@
-SHELL := /bin/bash
+SHELL := /usr/bin/env bash
AGDA := $(shell find . -type f -and \( -path '*/src/*' -or -path '*/courses/*' \) -and -name '*.lagda.md')
AGDAI := $(shell find . -type f -and \( -path '*/src/*' -or -path '*/courses/*' \) -and -name '*.agdai')
MARKDOWN := $(subst courses/,out/,$(subst src/,out/,$(subst .lagda.md,.md,$(AGDA))))
diff --git a/courses/tspl/2019/tspl2019.md b/courses/tspl/2019/tspl2019.md
index 97ab181b..93ffb328 100644
--- a/courses/tspl/2019/tspl2019.md
+++ b/courses/tspl/2019/tspl2019.md
@@ -8,8 +8,9 @@ permalink : /TSPL/2019/
* **Instructor**
[Philip Wadler](https://homepages.inf.ed.ac.uk/wadler)
-* **Teaching assistant**
+* **Teaching assistants**
- [Wen Kokke](mailto:wen.kokke@ed.ac.uk)
+ - [Orestis Melkonian](mailto:o.melkonian@sms.ed.ac.uk)
## Lectures
diff --git a/courses/tspl/make_assignment.sh b/courses/tspl/make_assignment.sh
new file mode 100755
index 00000000..10f0928f
--- /dev/null
+++ b/courses/tspl/make_assignment.sh
@@ -0,0 +1,188 @@
+#!/usr/bin/env bash
+
+# TODO:
+# - put the exercises from each chapter in their own module
+# - replicate the imports from that module
+# - import that module hiding anything defined in an exercise section
+
+# This script can be used to automatically generate assignment files from PLFA source files.
+# It takes a course abbreviation, e.g. TSPL, a year, and the number of the assignment.
+# At the moment, it outputs the University of Edinburgh guidelines for good scholarly practice,
+# making it somewhat specific to courses run there, but the header should be easy to edit.
+#
+# Usage:
+#
+# ./make_assignment.sh [COURSE_NAME] [COURSE_YEAR] [ASSIGNMENT_NUMBER] [PLFA_SOURCE_FILE...]
+
+COURSE="$1"
+shift
+
+YEAR="$1"
+shift
+
+NUM="$1"
+shift
+
+## Make assignment header
+
+cat <<-EOF
+---
+title : "Assignment$NUM: $COURSE Assignment $NUM"
+layout : page
+permalink : /$COURSE/$YEAR/Assignment$NUM/
+---
+
+\`\`\`
+module Assignment$NUM where
+\`\`\`
+
+## YOUR NAME AND EMAIL GOES HERE
+
+## Introduction
+
+You must do _all_ the exercises labelled "(recommended)".
+
+Exercises labelled "(stretch)" are there to provide an extra challenge.
+You don't need to do all of these, but should attempt at least a few.
+
+Exercises labelled "(practice)" are included for those who want extra practice.
+
+Submit your homework using the "submit" command.
+Please ensure your files execute correctly under Agda!
+
+
+## Good Scholarly Practice.
+
+Please remember the University requirement as
+regards all assessed work. Details about this can be found at:
+
+> [http://web.inf.ed.ac.uk/infweb/admin/policies/academic-misconduct](http://web.inf.ed.ac.uk/infweb/admin/policies/academic-misconduct)
+
+Furthermore, you are required to take reasonable measures to protect
+your assessed work from unauthorised access. For example, if you put
+any such work on a public repository then you must set access
+permissions appropriately (generally permitting access only to
+yourself, or your group in the case of group practicals).
+
+EOF
+
+## Awk Scripts
+
+AWK_GET_IMPORTS='
+ /^#/ {
+ import=0
+ }
+ /^## Imports/ {
+ import=1
+ }
+ /^```/ {
+ code=!code;
+ {
+ if (import)
+ print $0
+ };
+ next
+ }
+ {
+ if (import) {
+ if (code)
+ print " "$0
+ else
+ print $0
+ }
+ }
+'
+
+AWK_GET_DEFNS='
+ /^#/ {
+ exercise=0
+ }
+ /^#### Exercise/ {
+ exercise=1
+ }
+ /^```/ {
+ code=!code;
+ next
+ }
+ !/^ / {
+ postulate=0
+ }
+ /^postulate/ {
+ postulate=1
+ }
+ /^ [^ :(){}]+ +:/ {
+ if (exercise && code && postulate)
+ print $0
+ }
+ /^[^ :(){}]+ +:/ {
+ if (exercise && code)
+ print $0
+ }
+'
+
+AWK_GET_EXERCISES='
+ /^#/ {
+ exercise=0
+ }
+ /^#### Exercise/ {
+ exercise=1
+ }
+ /^```/ {
+ code=!code;
+ {
+ if (exercise)
+ print $0
+ };
+ next
+ }
+ {
+ if (exercise) {
+ if (code)
+ print " "$0
+ else
+ print $0
+ }
+ }
+'
+
+## Exercises
+
+for SRC in "$@"; do
+
+ # Generate Section & Module Header
+ NAME=$(basename "${SRC%.lagda.md}")
+ echo
+ echo "## $NAME"
+ echo
+ echo '```'
+ echo "module $NAME where"
+ echo '```'
+ echo
+
+ # Extract Imports
+ awk "$AWK_GET_IMPORTS" "$SRC"
+
+ # Generate Import and Hiding List
+ echo '```'
+ AGDA_MODULE=$(eval "echo \"$SRC\" | sed -e \"s|src/||g; s|\\\.lagda\\\.md||g; s|/|\\\.|g;\"")
+ echo " open import $AGDA_MODULE"
+ HIDING_LIST=""
+ OLDIFS=$IFS
+ IFS=$(echo -en "\n\b")
+ for defn in `awk "$AWK_GET_DEFNS" "$SRC"`;
+ do
+ NEW=$(eval "echo \"$defn\" | cut -d: -f1 | xargs")
+ if [ -z "$HIDING_LIST" ]; then
+ HIDING_LIST="$NEW"
+ else
+ HIDING_LIST="$HIDING_LIST; $NEW"
+ fi
+ done
+ IFS=$OLDIFS
+ echo " hiding ($HIDING_LIST)"
+ echo '```'
+ echo
+
+ # Extract Exercises
+ awk "$AWK_GET_EXERCISES" "$SRC"
+done
diff --git a/courses/tspl/send_marks.sh b/courses/tspl/send_marks.sh
new file mode 100755
index 00000000..516c4e73
--- /dev/null
+++ b/courses/tspl/send_marks.sh
@@ -0,0 +1,49 @@
+#!/usr/bin/env bash
+
+# Sends out marks for students based on the folder structure used by Submit,
+# the coursework submission system used in the School of Informatics at the
+# University of Edinburgh.
+#
+# This script assumes the following folder structure:
+#
+# $DIR/sXXXXXXX/cw$CW/$FILE
+#
+# The variable DIR refers to the directory passed in as an argument to the
+# script. The variable XXXXXXX refers to the student ID, and it is assumed
+# that
+#
+# sXXXXXXX@sms.ed.ac.uk
+#
+# is a valid email address. The variable $CW refers to the number for of the
+# coursework of which the students are meant to be notified. The directory
+# DIR/sXXXXXXX/cwY/ should only contain a single file, which should be
+# specified using the FILE parameter.
+#
+# Usage:
+#
+# ./send_marks.sh [DIR] [CW] [FILE]
+
+DIR="$1"
+shift
+
+CW="$1"
+shift
+
+FILE="$1"
+shift
+
+for ATTACHMENT in "${DIR%/}/s"*"/cw$CW/$FILE"; do
+ SUBJ="Mark for coursework $CW"
+ BODY=""
+ SID=$(echo "$ATTACHMENT" | sed 's|.*/\(s[0-9]\{7\}\)/.*|\1|')
+ ADDR="$SID@sms.ed.ac.uk"
+ CMD="echo \"$BODY\" | mail -s \"$SUBJ\" -a \"$ATTACHMENT\" \"$ADDR\""
+ echo "You are about to run the following command:"
+ echo -e "\n$CMD\n"
+ read -p "Are you sure? " -n 1 -r
+ echo
+ if [[ $REPLY =~ ^[Yy]$ ]]
+ then
+ eval "$CMD"
+ fi
+done
diff --git a/make_assignment.sh b/make_assignment.sh
deleted file mode 100755
index 40b5be3f..00000000
--- a/make_assignment.sh
+++ /dev/null
@@ -1,91 +0,0 @@
-#!/bin/bash
-
-# This script can be used to automatically generate assignment files from PLFA source files.
-# It takes a course abbreviation, e.g. TSPL, a year, and the number of the assignment.
-# At the moment, it outputs the University of Edinburgh guidelines for good scholarly practice,
-# making it somewhat specific to courses run there, but the header should be easy to edit.
-#
-# Usage:
-#
-# ./make_assignment.sh [COURSE_NAME] [COURSE_YEAR] [ASSIGNMENT_NUMBER] [PLFA_SOURCE_FILE...]
-
-COURSE="$1"
-shift
-
-YEAR="$1"
-shift
-
-NUM="$1"
-shift
-
-## Make assignment header
-
-cat <<-EOF
----
-title : "Assignment$NUM: $COURSE Assignment $NUM"
-layout : page
-permalink : /$COURSE/$YEAR/Assignment$NUM/
----
-
-\`\`\`
-module Assignment$NUM where
-\`\`\`
-
-## YOUR NAME AND EMAIL GOES HERE
-
-## Introduction
-
-You must do _all_ the exercises labelled "(recommended)".
-
-Exercises labelled "(stretch)" are there to provide an extra challenge.
-You don't need to do all of these, but should attempt at least a few.
-
-Exercises labelled "(practice)" are included for those who want extra practice.
-
-Submit your homework using the "submit" command.
-Please ensure your files execute correctly under Agda!
-
-
-## Good Scholarly Practice.
-
-Please remember the University requirement as
-regards all assessed work. Details about this can be found at:
-
-> [http://web.inf.ed.ac.uk/infweb/admin/policies/academic-misconduct](http://web.inf.ed.ac.uk/infweb/admin/policies/academic-misconduct)
-
-Furthermore, you are required to take reasonable measures to protect
-your assessed work from unauthorised access. For example, if you put
-any such work on a public repository then you must set access
-permissions appropriately (generally permitting access only to
-yourself, or your group in the case of group practicals).
-
-EOF
-
-## Make import statements
-
-cat <<-EOF
-
-## Imports
-
-\`\`\`
-EOF
-for SRC in "$@"; do
- AGDA_MODULE=$(eval "echo \"$SRC\" | sed -e \"s|src/||g; s|\\\.lagda\\\.md||g; s|/|\\\.|g;\"")
- echo "open import $AGDA_MODULE"
-done
-cat <<-EOF
-\`\`\`
-
-EOF
-
-## Extract exercises
-
-for SRC in "$@"; do
- NAME=$(basename "${SRC%.lagda.md}")
- cat <<-EOF
-
-## $NAME
-
-EOF
- awk '/^#/{flag=0} /^#### Exercise/{flag=1} flag' "$SRC"
-done
diff --git a/src/plfa/part1/Lists.lagda.md b/src/plfa/part1/Lists.lagda.md
index 2d01edec..de388e4f 100644
--- a/src/plfa/part1/Lists.lagda.md
+++ b/src/plfa/part1/Lists.lagda.md
@@ -656,7 +656,7 @@ Show
foldr _∷_ [] xs ≡ xs
-Show as a consequence of `foldr-++ above that
+Show as a consequence of `foldr-++` above that
xs ++ ys ≡ foldr _∷_ ys xs
diff --git a/src/plfa/part1/Naturals.lagda.md b/src/plfa/part1/Naturals.lagda.md
index a2b81f27..dc9cea37 100644
--- a/src/plfa/part1/Naturals.lagda.md
+++ b/src/plfa/part1/Naturals.lagda.md
@@ -913,7 +913,7 @@ between the two representations.
from : Bin → ℕ
For the former, choose the bitstring to have no leading zeros if it
-represents a positive natural, and represent zero by `x0 nil`.
+represents a positive natural, and represent zero by `⟨⟩ O`.
Confirm that these both give the correct answer for zero through four.
```
diff --git a/src/plfa/part2/Inference.lagda.md b/src/plfa/part2/Inference.lagda.md
index 654f497b..aabd52ff 100644
--- a/src/plfa/part2/Inference.lagda.md
+++ b/src/plfa/part2/Inference.lagda.md
@@ -169,7 +169,7 @@ checks that the inherited and synthesised types match.
Similarly, we said above that the function of an application is typed
by synthesis and that abstractions are typed by inheritance, giving a
-mismatch if the function of an application is a variable. Hence, we
+mismatch if the function of an application is an abstraction. Hence, we
need a way to treat an inherited term as if it is synthesised. We
introduce a new term form `M ↓ A` for this purpose. The typing
judgment returns `A` as the synthesized type of the term as a whole,