diff --git a/Makefile b/Makefile
index 9326d0f7..2bdb8ec0 100644
--- a/Makefile
+++ b/Makefile
@@ -1,7 +1,7 @@
 SHELL := /bin/bash
-agda := $(shell find . -type f -and \( -path '*/src/*' -or -path '*/tspl/*' \) -and -name '*.lagda.md')
-agdai := $(shell find . -type f -and \( -path '*/src/*' -or -path '*/tspl/*' \) -and -name '*.agdai')
-markdown := $(subst tspl/,out/,$(subst src/,out/,$(subst .lagda,,$(agda))))
+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))))
 PLFA_DIR := $(shell dirname $(realpath $(lastword $(MAKEFILE_LIST))))
 AGDA2HTML_FLAGS := --verbose --link-to-local-agda-names --use-jekyll=out/
 AGDA_STDLIB_SED := ".agda-stdlib.sed"
@@ -12,6 +12,7 @@ else
 AGDA_STDLIB_URL := https://agda.github.io/agda-stdlib/v$(AGDA_STDLIB_VERSION)/
 endif
 
+
 # Build PLFA and test hyperlinks
 test: build
 	ruby -S bundle exec htmlproofer _site
@@ -30,14 +31,24 @@ out/:
 	mkdir -p out/
 
 
-# Build PLFA pages
-out/%.md: src/%.lagda.md | out/
-	./highlight.sh $< $@
+# Convert literal Agda to Markdown
+define AGDA_template
+in := $(1)
+out := $(subst courses/,out/,$(subst src/,out/,$(subst .lagda.md,.md,$(1))))
+$$(out) : in  = $(1)
+$$(out) : out = $(subst courses/,out/,$(subst src/,out/,$(subst .lagda.md,.md,$(1))))
+$$(out) : $$(in) | out/
+	@echo "Processing $$(subst ./,,$$(in))"
+ifeq (,$$(findstring courses/,$$(in)))
+	./highlight.sh $$(in) $$(out)
+else
+# Fix links to the file itself (out/<filename> to out/<filepath>)
+	./highlight.sh $$(in) $$(out) --include-path $(realpath src) --include-path $$(realpath $$(dir $$(in)))
+	@sed -i 's|out/$$(notdir $$(out))|$$(subst ./,,$$(out))|g' $$(out)
+endif
+endef
 
-
-# Build TSPL pages
-out/%.md: tspl/%.lagda.md | out/
-	./highlight.sh $< $@ --include-path $(realpath src) --include-path $(realpath tspl)
+$(foreach agda,$(AGDA),$(eval $(call AGDA_template,$(agda))))
 
 
 # Start server
@@ -57,26 +68,26 @@ server-stop:
 
 # Build website using jekyll
 build: AGDA2HTML_FLAGS += --link-to-agda-stdlib=$(AGDA_STDLIB_URL)
-build: $(markdown)
+build: $(MARKDOWN)
 	ruby -S bundle exec jekyll build
 
 
 # Build website using jekyll offline
-build-offline: $(markdown)
+build-offline: $(MARKDOWN)
 	ruby -S bundle exec jekyll build
 
 
 # Build website using jekyll incrementally
 build-incremental: AGDA2HTML_FLAGS += --link-to-agda-stdlib
-build-incremental: $(markdown)
+build-incremental: $(MARKDOWN)
 	ruby -S bundle exec jekyll build --incremental
 
 
 # Remove all auxiliary files
 clean:
 	rm -f $(AGDA_STDLIB_SED)
-ifneq ($(strip $(agdai)),)
-	rm $(agdai)
+ifneq ($(strip $(AGDAI)),)
+	rm $(AGDAI)
 endif
 
 
@@ -90,7 +101,7 @@ clobber: clean
 
 # List all .lagda files
 ls:
-	@echo $(agda)
+	@echo $(AGDA)
 
 .phony: ls
 
diff --git a/tspl/Padova.lagda b/courses/padova/2019/padova2019.md
similarity index 100%
rename from tspl/Padova.lagda
rename to courses/padova/2019/padova2019.md
diff --git a/tspl/PUC-Assignment1.lagda.md b/courses/puc/2019/Assignment1.lagda.md
similarity index 97%
rename from tspl/PUC-Assignment1.lagda.md
rename to courses/puc/2019/Assignment1.lagda.md
index 90fc3d4f..f2d6f269 100644
--- a/tspl/PUC-Assignment1.lagda.md
+++ b/courses/puc/2019/Assignment1.lagda.md
@@ -1,11 +1,11 @@
 ---
-title     : "PUC-Assignment1: PUC Assignment 1"
+title     : "Assignment1: PUC Assignment 1"
 layout    : page
-permalink : /PUC-Assignment1/
+permalink : /PUC/2019/Assignment1/
 ---
 
 ```
-module PUC-Assignment1 where
+module Assignment1 where
 ```
 
 ## YOUR NAME AND EMAIL GOES HERE
@@ -122,7 +122,7 @@ Give an example of an operator that has an identity and is
 associative but is not commutative.
 
 
-#### Exercise `finite-+-assoc` (stretch) {#finite-plus-assoc}
+#### Exercise `finite-|-assoc` (stretch) {#finite-plus-assoc}
 
 Write out what is known about associativity of addition on each of the first four
 days using a finite story of creation, as
@@ -176,7 +176,7 @@ Show
 
 for all naturals `n`. Did your proof require induction?
 
-#### Exercise `∸-+-assoc` {#monus-plus-assoc}
+#### Exercise `∸-|-assoc` {#monus-plus-assoc}
 
 Show that monus associates with addition, that is,
 
diff --git a/tspl/PUC-Assignment2.lagda.md b/courses/puc/2019/Assignment2.lagda.md
similarity index 99%
rename from tspl/PUC-Assignment2.lagda.md
rename to courses/puc/2019/Assignment2.lagda.md
index e01a988e..1aa06905 100644
--- a/tspl/PUC-Assignment2.lagda.md
+++ b/courses/puc/2019/Assignment2.lagda.md
@@ -1,11 +1,11 @@
 ---
-title     : "PUC-Assignment2: PUC Assignment 2"
+title     : "Assignment2: PUC Assignment 2"
 layout    : page
-permalink : /PUC-Assignment2/
+permalink : /PUC/2019/Assignment2/
 ---
 
 ```
-module PUC-Assignment2 where
+module Assignment2 where
 ```
 
 ## YOUR NAME AND EMAIL GOES HERE
diff --git a/tspl/PUC-Assignment3.lagda.md b/courses/puc/2019/Assignment3.lagda.md
similarity index 98%
rename from tspl/PUC-Assignment3.lagda.md
rename to courses/puc/2019/Assignment3.lagda.md
index 2971a33b..d43acb6a 100644
--- a/tspl/PUC-Assignment3.lagda.md
+++ b/courses/puc/2019/Assignment3.lagda.md
@@ -1,11 +1,11 @@
 ---
-title     : "PUC-Assignment3: PUC Assignment 3"
+title     : "Assignment3: PUC Assignment 3"
 layout    : page
-permalink : /PUC-Assignment3/
+permalink : /PUC/2019/Assignment3/
 ---
 
 ```
-module PUC-Assignment3 where
+module Assignment3 where
 ```
 
 ## YOUR NAME AND EMAIL GOES HERE
diff --git a/tspl/PUC-Assignment4.lagda.md b/courses/puc/2019/Assignment4.lagda.md
similarity index 99%
rename from tspl/PUC-Assignment4.lagda.md
rename to courses/puc/2019/Assignment4.lagda.md
index 2514e673..6d68956b 100644
--- a/tspl/PUC-Assignment4.lagda.md
+++ b/courses/puc/2019/Assignment4.lagda.md
@@ -1,11 +1,11 @@
 ---
-title     : "PUC-Assignment4: PUC Assignment 4"
+title     : "Assignment4: PUC Assignment 4"
 layout    : page
-permalink : /PUC-Assignment4/
+permalink : /PUC/2019/Assignment4/
 ---
 
 ```
-module PUC-Assignment4 where
+module Assignment4 where
 ```
 
 ## YOUR NAME AND EMAIL GOES HERE
diff --git a/tspl/PUC-Assignment5.lagda.md b/courses/puc/2019/Assignment5.lagda.md
similarity index 99%
rename from tspl/PUC-Assignment5.lagda.md
rename to courses/puc/2019/Assignment5.lagda.md
index 4c2894b9..f915c2a7 100644
--- a/tspl/PUC-Assignment5.lagda.md
+++ b/courses/puc/2019/Assignment5.lagda.md
@@ -1,11 +1,11 @@
 ---
-title     : "PUC-Assignment5: PUC Assignment 5"
+title     : "Assignment5: PUC Assignment 5"
 layout    : page
-permalink : /PUC-Assignment5/
+permalink : /PUC/2019/Assignment5/
 ---
 
 ```
-module PUC-Assignment5 where
+module Assignment5 where
 ```
 
 ## YOUR NAME AND EMAIL GOES HERE
diff --git a/tspl/Exam.lagda.md b/courses/puc/2019/Exam.lagda.md
similarity index 99%
rename from tspl/Exam.lagda.md
rename to courses/puc/2019/Exam.lagda.md
index bd85d351..26ab3dfb 100644
--- a/tspl/Exam.lagda.md
+++ b/courses/puc/2019/Exam.lagda.md
@@ -1,7 +1,7 @@
 ---
 title     : "Exam: TSPL Mock Exam file"
 layout    : page
-permalink : /Exam/
+permalink : /PUC/2019/Exam/
 ---
 
 
diff --git a/tspl/instructions.tex b/courses/puc/2019/Instructions.tex
similarity index 98%
rename from tspl/instructions.tex
rename to courses/puc/2019/Instructions.tex
index 5e924fc8..8e845dd9 100644
--- a/tspl/instructions.tex
+++ b/courses/puc/2019/Instructions.tex
@@ -92,7 +92,7 @@ You are recommended to save your work on a regular basis.
   correctly. Code which prevents the file from compiling should be
   made into comments. If you fail to solve part of a problem, you
   may get more credit if you indicate clearly which part you have
-  not solved. 
+  not solved.
 
 \item \emph{Please ensure before submission that the file}
   \texttt{Exam.lagda} \emph{contains your solutions to the exam.}  Submit
@@ -104,7 +104,7 @@ You are recommended to save your work on a regular basis.
   \texttt{Exam.lagda} and that you are in the same directory as this
   file. If you continue to have problems, please contact one of the
   invigilators.
- 
+
 Repeated submit commands are allowed, and will overwrite previous
 submissions.  The last file submitted will be the one marked.
 
@@ -116,7 +116,7 @@ submissions.  The last file submitted will be the one marked.
 \end{document}
 
 
-%%% Local Variables: 
+%%% Local Variables:
 %%% mode: latex
 %%% TeX-master: t
-%%% End: 
+%%% End:
diff --git a/tspl/first-mock.tex b/courses/puc/2019/Mock1.tex
similarity index 94%
rename from tspl/first-mock.tex
rename to courses/puc/2019/Mock1.tex
index ee9e2e61..7991fc42 100644
--- a/tspl/first-mock.tex
+++ b/courses/puc/2019/Mock1.tex
@@ -1,422 +1,421 @@
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-% I N F O R M A T I C S
-%  Honours Exam LaTeX Template for Exam Authors
-%
-%  Created: 12-Oct-2009 by G.O.Passmore.
-%  Last Updated: 10-Sep-2018 by I. Murray
-%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%% The following define the status of the exam papers in the order
-%%% required.  Simply remove the comment (i.e., the % symbol) just
-%%% before the appropriate one and comment the others out.
-
-%\newcommand\status{\internal}
-%\newcommand\status{\external}
-\newcommand\status{\final}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%% The following three lines are always required.  You may add
-%%% custom packages to the one already defined if necessary.
-
-\documentclass{examhons2018}
-\usepackage{amssymb}
-\usepackage{amsmath}
-\usepackage{semantic}
-\usepackage{stix}
-
-%%% Uncomment the \checkmarksfalse line if the macros that check the
-%%% mark totals cause problems. However, please do not make your
-%%% questions add up to a non-standard number of marks without
-%%% permission of the convenor.
-%\checkmarksfalse
-
-\begin{document}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-% Replace {ad} below with the ITO code for your course.  This will
-%  be used by the ITO LaTeX installation to install course-specific
-%  data into the exam versions it produces from this document.
-% 
-% Your choices are (in course title order):
-%
-%   {anlp}     - Acc. Natural Language Processing	            (MSc)
-%   {aleone}   - Adaptive Learning Environments 1              (Inf4)
-%   {adbs}     - Advanced Databases                            (Inf4)
-%   {av}       - Advanced Vision                               (Inf4)
-%   {av-dl}    - Advanced Vision - distance learning            (MSc)
-%   {apl}      - Advances in Programming Languages             (Inf4)
-%   {abs}      - Agent Based Systems [L10]                     (Inf3)
-%   {afds}     - Algorithmic Foundations of Data Science        (MSc)
-%   {agta}     - Algorithmic Game Theory and its Apps.          (MSc)
-%   {ads}      - Algorithms and Data Structures                (Inf3)
-%   {ad}       - Applied Databases                              (MSc)
-%   {aipf}     - Artificial Intelligence Present and Future     (MSc)
-%   {ar}       - Automated Reasoning 	                       (Inf3)
-%   {asr}      - Automatic Speech Recognition                  (Inf4)
-%   {bioone}   - Bioinformatics 1                               (MSc)
-%   {biotwo}   - Bioinformatics 2                               (MSc)
-%	{bdl}      - Blockchains and Distributed Ledgers		   (Inf4)
-%   {cqi}      - Categories and Quantum Informatics             (MSc)
-%   {copt}     - Compiler Opimisation [L11]                    (Inf4)
-%   {ct}       - Compiling Techniques                          (Inf3)
-%   {ccs}      - Computational Cognitive Science               (Inf3)
-%   {cmc}      - Computational Complexity                      (Inf4)
-%   {ca}       - Computer Algebra                              (Inf4)
-%   {cav}      - Computer Animation and Visualisation          (Inf4)
-%   {car}      - Computer Architecture                         (Inf3)
-%   {comn}     - Computer Comms. and Networks                  (Inf3)
-%   {cd}       - Computer Design                               (Inf3)
-%   {cg}       - Computer Graphics [L11]                       (Inf4)
-%   {cn}       - Computer Networking [L11]                     (Inf4)
-%   {cp}       - Computer Prog. Skills and Concepts         (nonhons)
-%   {cs}       - Computer Security                             (Inf3)
-%   {dds}      - Data, Design and Society                   (nonhons)
-%   {dme}      - Data Mining and Exploration                   (Msc)
-%   {dbs}      - Database Systems                              (Inf3)
-%   {dmr}      - Decision Making in Robots and Autonomous Agents(MSc)
-%   {dmmr}     - Discrete Maths. and Math. Reasoning        (nonhons)
-%   {ds}       - Distributed Systems [L11]                     (Inf4)
-%   {epl}      - Elements of Programming Languages             (Inf3)
-%   {es}       - Embedded Software                             (Inf4)
-%   {exc}      - Extreme Computing                             (Inf4)
-%   {fv}       - Formal Verification                           (Inf4)
-%   {fnlp}     - Foundations of Natural Language Processing    (Inf3)
-%   {hci}      - Human-Computer Interaction [L11]              (Inf4)
-%   {infonea}  - Informatics 1 - Introduction to Computation(nonhons)
-%   different sittings for INF1A programming exams
-%   {infoneapone}  - Informatics 1 - Introduction to Computation(nonhons)
-%   {infoneaptwo}  - Informatics 1 - Introduction to Computation(nonhons)
-%   {infoneapthree}  - Informatics 1 - Introduction to Computation(nonhons)
-%   {infonecg} - Informatics 1 - Cognitive Science          (nonhons)
-%   {infonecl} - Informatics 1 - Computation and Logic      (nonhons)
-%   {infoneda} - Informatics 1 - Data and Analysis          (nonhons)
-%   {infonefp} - Informatics 1 - Functional Programming     (nonhons)
-%   If there are two sittings of FP, use infonefpam for the first
-%   paper and infonefppm for the second sitting.
-%   {infoneop} - Informatics 1 - Object-Oriented Programming(nonhons)
-%   If there are two sittings of OOP, use infoneopam for the first
-%   paper and infoneoppm for the second sitting.
-%   {inftwoa}  - Informatics 2A: Proc. F&N Languages        (nonhons)
-%   {inftwob}  - Informatics 2B: Algs., D.Structs., Learning(nonhons)
-%   {inftwoccs}- Informatics 2C-CS: Computer Systems        (nonhons)
-%   {inftwocse}- Informatics 2C: Software Engineering       (nonhons)
-%   {inftwod}  - Informatics 2D: Reasoning and Agents       (nonhons)
-%   {iar}      - Intelligent Autonomous Robotics               (Inf4)
-%   {it}       - Information Theory                             (MSc)
-%   {imc}      - Introduction to Modern Cryptography           (Inf4)
-%   {iotssc}   - Internet of Things, Systems, Security and the Cloud   (Inf4)
-%   (iqc)      - Introduction to Quantum Computing             (Inf4)
-%   (itcs)     - Introduction to Theoretical Computer Science  (Inf3)
-%   {ivc}      - Image and Vision Computing			           (MSc)
-%   {ivr}      - Introduction to Vision and Robotics           (Inf3)
-%   {ivr-dl}   - Introduction to Vision and Robotics - distance learning (Msc)
-%   {iaml}     - Introductory Applied Machine Learning         (MSc)
-%   {iaml-dl}  - Introductory Applied Machine Learning - distance learning (MSc)
-%   {lpt}      - Logic Programming - Theory                    (Inf3)
-%   {lpp}      - Logic Programming - Programming               (Inf3)
-%   {mlpr}     - Machine Learning & Pattern Recognition        (Inf4)
-%   {mt}       - Machine Translation                           (Inf4)    
-%   {mi}       - Music Informatics                              (MSc)
-%   {nlu}      - Natural Language Understanding [L11]          (Inf4)
-%   {nc}       - Neural Computation                             (MSc)
-%   {nat}      - Natural Computing                              (MSc)
-%   {nluplus}  - Natural Language Understanding, Generation, and Machine Translation(MSc)
-%   {nip}      - Neural Information Processing                  (MSc)
-%   {os}       - Operating Systems                             (Inf3)
-%   {pa}       - Parallel Architectures [L11]                  (Inf4)
-%   {pdiot}    - Principles and Design of IoT Systems          (Inf4)
-%   {ppls}     - Parallel Prog. Langs. and Sys. [L11]          (Inf4)
-%   {pm}       - Performance Modelling                         (Inf4)  
-%   {pmr}      - Probabilistic Modelling and Reasoning          (MSc)
-%   {pi}       - Professional Issues                           (Inf3)
-%   {rc}       - Randomness and Computation                    (Inf4)
-%   {rl}       - Reinforcement Learning                         (MSc)
-%   {rlsc}     - Robot Learning and Sensorimotor Control        (MSc)
-%   {rss}      - Robotics: Science and Systems                  (MSc)
-%   {sp}       - Secure Programming                            (Inf4)
-%   {sws}      - Semantic Web Systems                          (Inf4)
-%   {stn}      - Social and Technological Networks             (Inf4)
-%   {sapm}     - Software Arch., Proc. and Mgmt. [L11]         (Inf4)
-%   {sdm}      - Software Design and Modelling                 (Inf3)
-%   {st}       - Software Testing                              (Inf3)
-%   {ttds}     - Text Technologies for Data Science            (Inf4)
-%   {tspl}     - Types and Semantics for Programming Langs.    (Inf4)
-%   {usec}     - Usable Security and Privacy                   (Inf4)
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-\setcourse{tspl}
-\initcoursedata
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-% Set your exam rubric type.
-% 
-% Most courses in the School have exams that add up to 50 marks,
-% and your choices are:
-%    {qu1_and_either_qu2_or_qu3, any_two_of_three, do_exam}
-% (which include the "CALCULATORS MAY NOT BE USED..." text), or
-%    {qu1_and_either_qu2_or_qu3_calc, any_two_of_three_calc, do_exam_calc}
-% (which DO NOT include the "CALCULATORS MAY NOT BE USED..." text), or
-%    {custom}.
-%
-% Note, if you opt to create a custom rubric, you must: 
-%    
-%   (i) **have permission** from the appropriate authority, and 
-%  (ii) execute:
-%
-%        \setrubrictype{} to specify the custom rubric information.
-% 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-\setrubric{qu1_and_either_qu2_or_qu3}
-
-\examtitlepage
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-% Manual override for total page number computation.
-%
-% As long as you run latex upon this document three times in a row,
-%  the right number of `total pages' should be computed and placed
-%  in the footer of all pages except the title page.  
-%
-% But, if this fails, you can set that number yourself with the 
-%  following command:
-%
-%    \settotalpages{n} with n a natural number.
-%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-% Beginning of your exam text.
-%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-\begin{enumerate}
- 
-\item \rubricqA
-
-\newcommand{\Tree}{\texttt{Tree}}
-\newcommand{\AllT}{\texttt{AllT}}
-\newcommand{\AnyT}{\texttt{AnyT}}
-\newcommand{\leaf}{\texttt{leaf}}
-\newcommand{\branch}{\texttt{branch}}  
-\newcommand{\here}{\texttt{here}}
-\renewcommand{\left}{\texttt{left}}
-\renewcommand{\right}{\texttt{right}}
-\newcommand{\ubar}{\texttt{\underline{~}}}
-
-Consider a type of trees defined as follows.
-\begin{gather*}
-%
-  \inference[\leaf]
-    {A}
-    {Tree~A}
-%
-\quad
-%    
-  \inference[\ubar\branch\ubar]
-    {Tree~A \\
-     Tree~A}
-   {Tree~A}
-%
-\end{gather*}
-
-Given a predicate $P$ over $A$, we define predicates $\AllT$ and
-$\AnyT$ which hold when $P$ holds for \emph{every} leaf in the tree
-and when $P$ holds for \emph{some} leaf in the tree, respectively.
-\begin{gather*}
-%
-  \inference[\leaf]
-    {P~x}
-    {\AllT~P~(\leaf~x)}
-%
-\quad
-%    
-  \inference[\ubar\branch\ubar]
-    {\AllT~P~xt \\   
-     \AllT~P~yt}
-    {\AllT~P~(xt~\branch~yt)}
-%  
-\\~\\  
-%
-  \inference[\leaf]
-    {P~x}
-    {\AnyT~P~(\leaf~x)}
-%
-\quad
-%    
-  \inference[\left]
-    {\AnyT~P~xt}  
-    {\AnyT~P~(xt~\branch~yt)}
-%
-\quad
-%    
-  \inference[\right]
-    {\AnyT~P~yt}  
-    {\AnyT~P~(xt~\branch~yt)}
-%
-\end{gather*}    
-
-\begin{itemize}
-
-\item[(a)] Formalise the definitions above.
-
-\marks{12}
-
-\item[(b)] Prove $\AllT~({\neg\ubar}~\circ~P)~xt$
-  implies $\neg~(\AnyT~P~xt)$, for all trees $xt$.
-
-\marks{13}
-
-\end{itemize}
-
-\newpage
-
-\item \rubricqB
-
-\newcommand{\COMP}{\texttt{Comp}}
-\newcommand{\OK}{\texttt{ok}}
-\newcommand{\ERROR}{\texttt{error}}
-\newcommand{\LETC}{\texttt{letc}}
-\newcommand{\IN}{\texttt{in}}  
-
-\newcommand{\Comp}[1]{\COMP~#1}
-\newcommand{\error}[1]{\ERROR~#1}
-\newcommand{\ok}[1]{\OK~#1}
-\newcommand{\letc}[3]{\LETC~#1\leftarrow#2~\IN~#3}
-
-\newcommand{\comma}{\,,\,}
-\newcommand{\V}{\texttt{V}}
-\newcommand{\dash}{\texttt{-}}
-\newcommand{\Value}{\texttt{Value}}
-\newcommand{\becomes}{\longrightarrow}
-\newcommand{\subst}[3]{#1~\texttt{[}~#2~\texttt{:=}~#3~\texttt{]}}
-
-You will be provided with a definition of intrinsically-typed lambda
-calculus in Agda. Consider constructs satisfying the following rules,
-written in extrinsically-typed style.
-
-A computation of type $\Comp{A}$ returns either an error with a
-message $msg$ which is a string, or an ok value of a term $M$ of type $A$.
-Consider constructs satisfying the following rules:
-
-Typing:
-\begin{gather*}
-\inference[$\ERROR$]
-  {}
-  {\Gamma \vdash \error{msg} \typecolon \Comp{A}}
-\qquad
-\inference[$\OK$]
-  {\Gamma \vdash M \typecolon A}
-  {\Gamma \vdash \ok{M} \typecolon \Comp{A}}
-\\~\\
-\inference[$\LETC$]
-  {\Gamma \vdash M \typecolon \Comp{A} \\
-   \Gamma \comma x \typecolon A \vdash N \typecolon \Comp{B}}
-  {\Gamma \vdash \letc{x}{M}{N} \typecolon \Comp{B}}
-\end{gather*}
-
-Values:
-\begin{gather*}
-\inference[\V\dash\ERROR]
-  {}
-  {\Value~(\error{msg})}
-\qquad
-\inference[\V\dash\OK]
-  {\Value~V}
-  {\Value~(\ok{V})}
-\end{gather*}
-
-Reduction:
-\begin{gather*}
-\inference[$\xi\dash\OK$]
-  {M \becomes M'}
-  {\ok{M} \becomes \ok{M'}}
-\qquad
-\inference[$\xi\dash\LETC$]
-  {M \becomes M'}
-  {\letc{x}{M}{N} \becomes \letc{x}{M'}{N}}
-\\~\\
-\inference[$\beta\dash\ERROR$]
-  {}
-  {\letc{x}{(\error{msg})}{t} \becomes \error{msg}}
-\\~\\
-\inference[$\beta\dash\OK$]
-  {\Value{V}}
-  {\letc{x}{(\ok{V})}{N} \becomes \subst{N}{x}{V}}
-\end{gather*}
-
-\begin{enumerate}
-\item[(a)] Extend the given definition to formalise the evaluation
-           and typing rules, including any other required definitions.
-      \marks{12}
-
-\item[(b)] Prove progress. You will be provided with a proof of progress for
-           the simply-typed lambda calculus that you may extend.
-      \marks{13}
-\end{enumerate}
-
-Please delimit any code you add as follows.
-\begin{verbatim}
--- begin
--- end
-\end{verbatim}
-
-\newpage
-
-\item \rubricqC
-
-\newcommand{\TT}{\texttt{tt}}
-\newcommand{\CASETOP}{{\texttt{case}\top}}
-\newcommand{\casetop}[2]{\CASETOP~#1~{\texttt{[tt}\!\Rightarrow}~#2~\texttt{]}}
-\newcommand{\up}{\uparrow}
-\newcommand{\dn}{\downarrow}
-
-You will be provided with a definition of inference for extrinsically-typed lambda
-calculus in Agda. Consider constructs satisfying the following rules,
-written in extrinsically-typed style that support bidirectional inference.
-
-Typing:
-\begin{gather*}
-\inference[$\TT$]
-  {}
-  {\Gamma \vdash \TT \dn \top}
-\\~\\
-\inference[$\CASETOP$]
-  {\Gamma \vdash L \up \top \\
-   \Gamma \vdash M \dn A}
-  {\Gamma \vdash \casetop{L}{M} \dn A} 
-\end{gather*}
-
-\begin{enumerate}
-\item[(a)] Extend the given definition to formalise the typing rules,
-      and update the definition of equality on types.
-      \marks{10}
-
-\item[(b)] Extend the code to support type inference for the new features.
-      \marks{15}
-\end{enumerate}
-
-Please delimit any code you add as follows.
-\begin{verbatim}
--- begin
--- end
-\end{verbatim}
-
-\end{enumerate}
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%
-% End of your exam text.
-%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-\end{document}
-
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% I N F O R M A T I C S
+%  Honours Exam LaTeX Template for Exam Authors
+%
+%  Created: 12-Oct-2009 by G.O.Passmore.
+%  Last Updated: 10-Sep-2018 by I. Murray
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%% The following define the status of the exam papers in the order
+%%% required.  Simply remove the comment (i.e., the % symbol) just
+%%% before the appropriate one and comment the others out.
+
+%\newcommand\status{\internal}
+%\newcommand\status{\external}
+\newcommand\status{\final}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%% The following three lines are always required.  You may add
+%%% custom packages to the one already defined if necessary.
+
+\documentclass{examhons2018}
+\usepackage{amssymb}
+\usepackage{amsmath}
+\usepackage{semantic}
+\usepackage{stix}
+
+%%% Uncomment the \checkmarksfalse line if the macros that check the
+%%% mark totals cause problems. However, please do not make your
+%%% questions add up to a non-standard number of marks without
+%%% permission of the convenor.
+%\checkmarksfalse
+
+\begin{document}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Replace {ad} below with the ITO code for your course.  This will
+%  be used by the ITO LaTeX installation to install course-specific
+%  data into the exam versions it produces from this document.
+%
+% Your choices are (in course title order):
+%
+%   {anlp}     - Acc. Natural Language Processing	            (MSc)
+%   {aleone}   - Adaptive Learning Environments 1              (Inf4)
+%   {adbs}     - Advanced Databases                            (Inf4)
+%   {av}       - Advanced Vision                               (Inf4)
+%   {av-dl}    - Advanced Vision - distance learning            (MSc)
+%   {apl}      - Advances in Programming Languages             (Inf4)
+%   {abs}      - Agent Based Systems [L10]                     (Inf3)
+%   {afds}     - Algorithmic Foundations of Data Science        (MSc)
+%   {agta}     - Algorithmic Game Theory and its Apps.          (MSc)
+%   {ads}      - Algorithms and Data Structures                (Inf3)
+%   {ad}       - Applied Databases                              (MSc)
+%   {aipf}     - Artificial Intelligence Present and Future     (MSc)
+%   {ar}       - Automated Reasoning 	                       (Inf3)
+%   {asr}      - Automatic Speech Recognition                  (Inf4)
+%   {bioone}   - Bioinformatics 1                               (MSc)
+%   {biotwo}   - Bioinformatics 2                               (MSc)
+%	{bdl}      - Blockchains and Distributed Ledgers		   (Inf4)
+%   {cqi}      - Categories and Quantum Informatics             (MSc)
+%   {copt}     - Compiler Opimisation [L11]                    (Inf4)
+%   {ct}       - Compiling Techniques                          (Inf3)
+%   {ccs}      - Computational Cognitive Science               (Inf3)
+%   {cmc}      - Computational Complexity                      (Inf4)
+%   {ca}       - Computer Algebra                              (Inf4)
+%   {cav}      - Computer Animation and Visualisation          (Inf4)
+%   {car}      - Computer Architecture                         (Inf3)
+%   {comn}     - Computer Comms. and Networks                  (Inf3)
+%   {cd}       - Computer Design                               (Inf3)
+%   {cg}       - Computer Graphics [L11]                       (Inf4)
+%   {cn}       - Computer Networking [L11]                     (Inf4)
+%   {cp}       - Computer Prog. Skills and Concepts         (nonhons)
+%   {cs}       - Computer Security                             (Inf3)
+%   {dds}      - Data, Design and Society                   (nonhons)
+%   {dme}      - Data Mining and Exploration                   (Msc)
+%   {dbs}      - Database Systems                              (Inf3)
+%   {dmr}      - Decision Making in Robots and Autonomous Agents(MSc)
+%   {dmmr}     - Discrete Maths. and Math. Reasoning        (nonhons)
+%   {ds}       - Distributed Systems [L11]                     (Inf4)
+%   {epl}      - Elements of Programming Languages             (Inf3)
+%   {es}       - Embedded Software                             (Inf4)
+%   {exc}      - Extreme Computing                             (Inf4)
+%   {fv}       - Formal Verification                           (Inf4)
+%   {fnlp}     - Foundations of Natural Language Processing    (Inf3)
+%   {hci}      - Human-Computer Interaction [L11]              (Inf4)
+%   {infonea}  - Informatics 1 - Introduction to Computation(nonhons)
+%   different sittings for INF1A programming exams
+%   {infoneapone}  - Informatics 1 - Introduction to Computation(nonhons)
+%   {infoneaptwo}  - Informatics 1 - Introduction to Computation(nonhons)
+%   {infoneapthree}  - Informatics 1 - Introduction to Computation(nonhons)
+%   {infonecg} - Informatics 1 - Cognitive Science          (nonhons)
+%   {infonecl} - Informatics 1 - Computation and Logic      (nonhons)
+%   {infoneda} - Informatics 1 - Data and Analysis          (nonhons)
+%   {infonefp} - Informatics 1 - Functional Programming     (nonhons)
+%   If there are two sittings of FP, use infonefpam for the first
+%   paper and infonefppm for the second sitting.
+%   {infoneop} - Informatics 1 - Object-Oriented Programming(nonhons)
+%   If there are two sittings of OOP, use infoneopam for the first
+%   paper and infoneoppm for the second sitting.
+%   {inftwoa}  - Informatics 2A: Proc. F&N Languages        (nonhons)
+%   {inftwob}  - Informatics 2B: Algs., D.Structs., Learning(nonhons)
+%   {inftwoccs}- Informatics 2C-CS: Computer Systems        (nonhons)
+%   {inftwocse}- Informatics 2C: Software Engineering       (nonhons)
+%   {inftwod}  - Informatics 2D: Reasoning and Agents       (nonhons)
+%   {iar}      - Intelligent Autonomous Robotics               (Inf4)
+%   {it}       - Information Theory                             (MSc)
+%   {imc}      - Introduction to Modern Cryptography           (Inf4)
+%   {iotssc}   - Internet of Things, Systems, Security and the Cloud   (Inf4)
+%   (iqc)      - Introduction to Quantum Computing             (Inf4)
+%   (itcs)     - Introduction to Theoretical Computer Science  (Inf3)
+%   {ivc}      - Image and Vision Computing			           (MSc)
+%   {ivr}      - Introduction to Vision and Robotics           (Inf3)
+%   {ivr-dl}   - Introduction to Vision and Robotics - distance learning (Msc)
+%   {iaml}     - Introductory Applied Machine Learning         (MSc)
+%   {iaml-dl}  - Introductory Applied Machine Learning - distance learning (MSc)
+%   {lpt}      - Logic Programming - Theory                    (Inf3)
+%   {lpp}      - Logic Programming - Programming               (Inf3)
+%   {mlpr}     - Machine Learning & Pattern Recognition        (Inf4)
+%   {mt}       - Machine Translation                           (Inf4)
+%   {mi}       - Music Informatics                              (MSc)
+%   {nlu}      - Natural Language Understanding [L11]          (Inf4)
+%   {nc}       - Neural Computation                             (MSc)
+%   {nat}      - Natural Computing                              (MSc)
+%   {nluplus}  - Natural Language Understanding, Generation, and Machine Translation(MSc)
+%   {nip}      - Neural Information Processing                  (MSc)
+%   {os}       - Operating Systems                             (Inf3)
+%   {pa}       - Parallel Architectures [L11]                  (Inf4)
+%   {pdiot}    - Principles and Design of IoT Systems          (Inf4)
+%   {ppls}     - Parallel Prog. Langs. and Sys. [L11]          (Inf4)
+%   {pm}       - Performance Modelling                         (Inf4)
+%   {pmr}      - Probabilistic Modelling and Reasoning          (MSc)
+%   {pi}       - Professional Issues                           (Inf3)
+%   {rc}       - Randomness and Computation                    (Inf4)
+%   {rl}       - Reinforcement Learning                         (MSc)
+%   {rlsc}     - Robot Learning and Sensorimotor Control        (MSc)
+%   {rss}      - Robotics: Science and Systems                  (MSc)
+%   {sp}       - Secure Programming                            (Inf4)
+%   {sws}      - Semantic Web Systems                          (Inf4)
+%   {stn}      - Social and Technological Networks             (Inf4)
+%   {sapm}     - Software Arch., Proc. and Mgmt. [L11]         (Inf4)
+%   {sdm}      - Software Design and Modelling                 (Inf3)
+%   {st}       - Software Testing                              (Inf3)
+%   {ttds}     - Text Technologies for Data Science            (Inf4)
+%   {tspl}     - Types and Semantics for Programming Langs.    (Inf4)
+%   {usec}     - Usable Security and Privacy                   (Inf4)
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\setcourse{tspl}
+\initcoursedata
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Set your exam rubric type.
+%
+% Most courses in the School have exams that add up to 50 marks,
+% and your choices are:
+%    {qu1_and_either_qu2_or_qu3, any_two_of_three, do_exam}
+% (which include the "CALCULATORS MAY NOT BE USED..." text), or
+%    {qu1_and_either_qu2_or_qu3_calc, any_two_of_three_calc, do_exam_calc}
+% (which DO NOT include the "CALCULATORS MAY NOT BE USED..." text), or
+%    {custom}.
+%
+% Note, if you opt to create a custom rubric, you must:
+%
+%   (i) **have permission** from the appropriate authority, and
+%  (ii) execute:
+%
+%        \setrubrictype{} to specify the custom rubric information.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\setrubric{qu1_and_either_qu2_or_qu3}
+
+\examtitlepage
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Manual override for total page number computation.
+%
+% As long as you run latex upon this document three times in a row,
+%  the right number of `total pages' should be computed and placed
+%  in the footer of all pages except the title page.
+%
+% But, if this fails, you can set that number yourself with the
+%  following command:
+%
+%    \settotalpages{n} with n a natural number.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Beginning of your exam text.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{enumerate}
+
+\item \rubricqA
+
+\newcommand{\Tree}{\texttt{Tree}}
+\newcommand{\AllT}{\texttt{AllT}}
+\newcommand{\AnyT}{\texttt{AnyT}}
+\newcommand{\leaf}{\texttt{leaf}}
+\newcommand{\branch}{\texttt{branch}}
+\newcommand{\here}{\texttt{here}}
+\renewcommand{\left}{\texttt{left}}
+\renewcommand{\right}{\texttt{right}}
+\newcommand{\ubar}{\texttt{\underline{~}}}
+
+Consider a type of trees defined as follows.
+\begin{gather*}
+%
+  \inference[\leaf]
+    {A}
+    {Tree~A}
+%
+\quad
+%
+  \inference[\ubar\branch\ubar]
+    {Tree~A \\
+     Tree~A}
+   {Tree~A}
+%
+\end{gather*}
+
+Given a predicate $P$ over $A$, we define predicates $\AllT$ and
+$\AnyT$ which hold when $P$ holds for \emph{every} leaf in the tree
+and when $P$ holds for \emph{some} leaf in the tree, respectively.
+\begin{gather*}
+%
+  \inference[\leaf]
+    {P~x}
+    {\AllT~P~(\leaf~x)}
+%
+\quad
+%
+  \inference[\ubar\branch\ubar]
+    {\AllT~P~xt \\
+     \AllT~P~yt}
+    {\AllT~P~(xt~\branch~yt)}
+%
+\\~\\
+%
+  \inference[\leaf]
+    {P~x}
+    {\AnyT~P~(\leaf~x)}
+%
+\quad
+%
+  \inference[\left]
+    {\AnyT~P~xt}
+    {\AnyT~P~(xt~\branch~yt)}
+%
+\quad
+%
+  \inference[\right]
+    {\AnyT~P~yt}
+    {\AnyT~P~(xt~\branch~yt)}
+%
+\end{gather*}
+
+\begin{itemize}
+
+\item[(a)] Formalise the definitions above.
+
+\marks{12}
+
+\item[(b)] Prove $\AllT~({\neg\ubar}~\circ~P)~xt$
+  implies $\neg~(\AnyT~P~xt)$, for all trees $xt$.
+
+\marks{13}
+
+\end{itemize}
+
+\newpage
+
+\item \rubricqB
+
+\newcommand{\COMP}{\texttt{Comp}}
+\newcommand{\OK}{\texttt{ok}}
+\newcommand{\ERROR}{\texttt{error}}
+\newcommand{\LETC}{\texttt{letc}}
+\newcommand{\IN}{\texttt{in}}
+
+\newcommand{\Comp}[1]{\COMP~#1}
+\newcommand{\error}[1]{\ERROR~#1}
+\newcommand{\ok}[1]{\OK~#1}
+\newcommand{\letc}[3]{\LETC~#1\leftarrow#2~\IN~#3}
+
+\newcommand{\comma}{\,,\,}
+\newcommand{\V}{\texttt{V}}
+\newcommand{\dash}{\texttt{-}}
+\newcommand{\Value}{\texttt{Value}}
+\newcommand{\becomes}{\longrightarrow}
+\newcommand{\subst}[3]{#1~\texttt{[}~#2~\texttt{:=}~#3~\texttt{]}}
+
+You will be provided with a definition of intrinsically-typed lambda
+calculus in Agda. Consider constructs satisfying the following rules,
+written in extrinsically-typed style.
+
+A computation of type $\Comp{A}$ returns either an error with a
+message $msg$ which is a string, or an ok value of a term $M$ of type $A$.
+Consider constructs satisfying the following rules:
+
+Typing:
+\begin{gather*}
+\inference[$\ERROR$]
+  {}
+  {\Gamma \vdash \error{msg} \typecolon \Comp{A}}
+\qquad
+\inference[$\OK$]
+  {\Gamma \vdash M \typecolon A}
+  {\Gamma \vdash \ok{M} \typecolon \Comp{A}}
+\\~\\
+\inference[$\LETC$]
+  {\Gamma \vdash M \typecolon \Comp{A} \\
+   \Gamma \comma x \typecolon A \vdash N \typecolon \Comp{B}}
+  {\Gamma \vdash \letc{x}{M}{N} \typecolon \Comp{B}}
+\end{gather*}
+
+Values:
+\begin{gather*}
+\inference[\V\dash\ERROR]
+  {}
+  {\Value~(\error{msg})}
+\qquad
+\inference[\V\dash\OK]
+  {\Value~V}
+  {\Value~(\ok{V})}
+\end{gather*}
+
+Reduction:
+\begin{gather*}
+\inference[$\xi\dash\OK$]
+  {M \becomes M'}
+  {\ok{M} \becomes \ok{M'}}
+\qquad
+\inference[$\xi\dash\LETC$]
+  {M \becomes M'}
+  {\letc{x}{M}{N} \becomes \letc{x}{M'}{N}}
+\\~\\
+\inference[$\beta\dash\ERROR$]
+  {}
+  {\letc{x}{(\error{msg})}{t} \becomes \error{msg}}
+\\~\\
+\inference[$\beta\dash\OK$]
+  {\Value{V}}
+  {\letc{x}{(\ok{V})}{N} \becomes \subst{N}{x}{V}}
+\end{gather*}
+
+\begin{enumerate}
+\item[(a)] Extend the given definition to formalise the evaluation
+           and typing rules, including any other required definitions.
+      \marks{12}
+
+\item[(b)] Prove progress. You will be provided with a proof of progress for
+           the simply-typed lambda calculus that you may extend.
+      \marks{13}
+\end{enumerate}
+
+Please delimit any code you add as follows.
+\begin{verbatim}
+-- begin
+-- end
+\end{verbatim}
+
+\newpage
+
+\item \rubricqC
+
+\newcommand{\TT}{\texttt{tt}}
+\newcommand{\CASETOP}{{\texttt{case}\top}}
+\newcommand{\casetop}[2]{\CASETOP~#1~{\texttt{[tt}\!\Rightarrow}~#2~\texttt{]}}
+\newcommand{\up}{\uparrow}
+\newcommand{\dn}{\downarrow}
+
+You will be provided with a definition of inference for extrinsically-typed lambda
+calculus in Agda. Consider constructs satisfying the following rules,
+written in extrinsically-typed style that support bidirectional inference.
+
+Typing:
+\begin{gather*}
+\inference[$\TT$]
+  {}
+  {\Gamma \vdash \TT \dn \top}
+\\~\\
+\inference[$\CASETOP$]
+  {\Gamma \vdash L \up \top \\
+   \Gamma \vdash M \dn A}
+  {\Gamma \vdash \casetop{L}{M} \dn A}
+\end{gather*}
+
+\begin{enumerate}
+\item[(a)] Extend the given definition to formalise the typing rules,
+      and update the definition of equality on types.
+      \marks{10}
+
+\item[(b)] Extend the code to support type inference for the new features.
+      \marks{15}
+\end{enumerate}
+
+Please delimit any code you add as follows.
+\begin{verbatim}
+-- begin
+-- end
+\end{verbatim}
+
+\end{enumerate}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% End of your exam text.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\end{document}
diff --git a/tspl/examhons2018.cls b/courses/puc/2019/examhons2018.cls
similarity index 94%
rename from tspl/examhons2018.cls
rename to courses/puc/2019/examhons2018.cls
index 857d30ce..73e31e10 100644
--- a/tspl/examhons2018.cls
+++ b/courses/puc/2019/examhons2018.cls
@@ -9,7 +9,7 @@
 %  Note: We are changing the file and package name of this style
 %   from year to year, so as to make people aware of the version
 %   they are using.  The format is `examhons<YYYY>.sty' with <YYYY>
-%   replaced appropriately. 
+%   replaced appropriately.
 %
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
@@ -20,14 +20,14 @@
 %
 % Set the ITO path for status.tex.
 %
-% * Note that course organisers / exam preparers do not need 
-%    status.tex.  When building their exam on their own machines, 
+% * Note that course organisers / exam preparers do not need
+%    status.tex.  When building their exam on their own machines,
 %    the exam title / date / etc. information will be automatically
-%    filled-in with dummy values for mock-up purposes. 
-% 
-%    Once the exam document is processed on the ITO machines, 
-%    however, the mock-up exam title / date / etc. data will be 
-%    overwritten with the officially sanctioned data held in 
+%    filled-in with dummy values for mock-up purposes.
+%
+%    Once the exam document is processed on the ITO machines,
+%    however, the mock-up exam title / date / etc. data will be
+%    overwritten with the officially sanctioned data held in
 %    the ITO's master status.tex file.
 %
 %  This file resides in the relative path below.
@@ -45,10 +45,10 @@
 \LoadClass[12pt,a4paper]{article}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% 
-% Take care of `page x of y' the proper way, based on a combination 
+%
+% Take care of `page x of y' the proper way, based on a combination
 %  of the J. Goldberg (lastpage) method, the C. Huggins (using fh)
-%  code, woven together with some use of the ifthen package for 
+%  code, woven together with some use of the ifthen package for
 %  branching on p0 (the exam title page, which shouldn't be num'd).
 %
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -63,7 +63,7 @@
    \addtocounter{page}{1}}
 
 \AtEndDocument{%
-   \message{*** Setting LastPage: Make sure you 
+   \message{*** Setting LastPage: Make sure you
      run LaTeX upon your exam file at least 3
      times to get this right.}%
    \clearpage\lastpage@putlabel}%
@@ -77,7 +77,7 @@
           {{\scriptsize{Page \thepage{} of \@forcedtotalpages}}}}}
 
 
-\renewcommand\headrulewidth{0pt}  
+\renewcommand\headrulewidth{0pt}
 
 \newcommand{\settotalpages}[1]{
  \def\@forcedtotalpages{#1}
@@ -168,7 +168,7 @@
 %   We have a sticky problem here:  TeX doesn't do floating point arithmetic!
 %   Our goal is to compute y = rx/t. The following loop does this reasonably
 %   fast, with an error of at most about 16 sp (about 1/4000 pt).
-% 
+%
      \else\epsftmp=\epsftsize \divide\epsftmp\epsfrsize
        \epsfxsize=\epsfysize \multiply\epsfxsize\epsftmp
        \multiply\epsftmp\epsfrsize \advance\epsftsize-\epsftmp
@@ -182,7 +182,7 @@
      \fi
    \else \ifnum\epsfysize=0
      \epsftmp=\epsfrsize \divide\epsftmp\epsftsize
-     \epsfysize=\epsfxsize \multiply\epsfysize\epsftmp   
+     \epsfysize=\epsfxsize \multiply\epsfysize\epsftmp
      \multiply\epsftmp\epsftsize \advance\epsfrsize-\epsftmp
      \epsftmp=\epsfxsize
      \loop \advance\epsfrsize\epsfrsize \divide\epsftmp 2
@@ -255,14 +255,14 @@
 %
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\def\@cent{\count0 }                      
-\def\@diy{\count1 }                        
-\def\@dow{\count2 }                        
-\def\@epact{\count3 }                      
-\def\@golden{\count4 }                     
-\def\@leap{\count5 }                       
-\def\@x{\count6 }                          
-\def\@y{\count7 }                          
+\def\@cent{\count0 }
+\def\@diy{\count1 }
+\def\@dow{\count2 }
+\def\@epact{\count3 }
+\def\@golden{\count4 }
+\def\@leap{\count5 }
+\def\@x{\count6 }
+\def\@y{\count7 }
 
 \def\@up#1{{\@savestyle\thinspace$^{\underline{\hbox{%
   \scriptsize\@setstyle#1\fam=-1 }}}$}}
@@ -288,7 +288,7 @@
   \advance\@leap by \year
   \@dow=\month \advance\@dow by 10
   \@y=\@dow \divide\@y by 13 \multiply\@y by 12
-  \advance\@dow by -\@y \multiply\@dow by 13 
+  \advance\@dow by -\@y \multiply\@dow by 13
   \advance\@dow by -1 \divide\@dow by 5
   \advance\@dow by \day \advance\@dow by 77
   \@x=\@leap \@y=\@x \divide\@y by 100 \multiply\@y by 100 \advance\@x by -\@y
@@ -299,25 +299,25 @@
   \ifcase\@dow Sunday\or Monday\or Tuesday\or Wednesday\or
       Thursday\or Friday\or Saturday\fi}}
 \def\phaseofmoon{{%
-  \@diy=\day \advance\@diy by \ifcase\month            
-      -1\or -1\or 30\or 58\or 89\or 119\or 150\or      
-      180\or 211\or 241\or 272\or 303\or 333\fi        
+  \@diy=\day \advance\@diy by \ifcase\month
+      -1\or -1\or 30\or 58\or 89\or 119\or 150\or
+      180\or 211\or 241\or 272\or 303\or 333\fi
   \ifnum \month>2
     \@x=\year \@y=\@x \divide\@y by 4 \multiply\@y by 4 \advance\@x by -\@y
-    \ifnum \@x=0                    
-      \@x=\year \@y=\@x \divide\@y by 400 
+    \ifnum \@x=0
+      \@x=\year \@y=\@x \divide\@y by 400
       \multiply\@y by 400 \advance\@x by -\@y
-      \ifnum \@x=0                  
-      \advance\@diy by 1            
-      \else                         
-      \@x=\year \@y=\@x \divide\@y by 100 
+      \ifnum \@x=0
+      \advance\@diy by 1
+      \else
+      \@x=\year \@y=\@x \divide\@y by 100
       \multiply\@y by 100 \advance\@x by -\@y
-      \ifnum \@x>0                  
-          \advance\@diy by 1        
-      \fi                           
-      \fi                           
-    \fi                             
-  \fi                               
+      \ifnum \@x>0
+          \advance\@diy by 1
+      \fi
+      \fi
+    \fi
+  \fi
   \@cent=\year \divide\@cent by 100 \advance\@cent by 1
   \@golden=\year
   \@y=\year \divide\@y by 19 \multiply\@y by 19 \advance\@golden by -\@y
@@ -356,13 +356,13 @@
 %  and so on, *but* we want to provide hard-coded dummy values
 %  for exam preparers who are working on their own machines.
 %  This is so that status.tex does not need to be ever copied from
-%  the ITO installation; it is only for ITO.  
+%  the ITO installation; it is only for ITO.
 %
 % The logic here is simple.  If we find \itostatuspath status.tex
 %  to exist, then we populate the values of exam title, time, and
 %  so on using those it contains corresponding to \courseid, which
 %  is set by the exam preparer using the \setcourse command.
-%  This is done internally by executing a command named 
+%  This is done internally by executing a command named
 %  \<courseid>details, with <courseid> replaced by their courseid.
 %
 % Otherwise, we use dummy values, but we've gone to the effort to
@@ -428,7 +428,7 @@
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %
-% Display the exam status (for `internal'/`external' scrutiny, or 
+% Display the exam status (for `internal'/`external' scrutiny, or
 %  `final' which will print no corresponding notice).
 %
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -445,11 +445,11 @@
 %
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\def\Marks#1#2{\marginpar{\raisebox{#2\baselineskip}{[{\it #1 
+\def\Marks#1#2{\marginpar{\raisebox{#2\baselineskip}{[{\it #1
   \ifnum #1=1 mark\else marks\fi\/}]}}}
 %Version for most situations.
 \def\marks#1{\Marks{#1}{0}}
-% The next version is to get around the problem that you cannot put a 
+% The next version is to get around the problem that you cannot put a
 % marginpar in maths display.  Put \marksl just before the display line.
 \def\marksd#1{\Marks{#1}{-2}}
 % As above but raises the box.
@@ -461,10 +461,10 @@
 %
 % EPS macros by KK.
 %
-% The first argument is the filename and the second the size (of the 
-%  x-axis or the y-axis respectively.  
+% The first argument is the filename and the second the size (of the
+%  x-axis or the y-axis respectively.
 %
-% For example \psfigx{graph1.epsf}{5in} will input your first graph 
+% For example \psfigx{graph1.epsf}{5in} will input your first graph
 %  and make the x-axis equal to 4.5in, with the y-axis appropriately
 %  scaled.
 %
@@ -476,7 +476,7 @@
      \epsfxsize=#2
      \epsffile{#1}
    \end{center}}
-   
+
 \def\psfigy#1#2{
   \begin{center}
      \leavevmode
@@ -492,7 +492,7 @@
 %  and otherwise will source the master ITO status.tex if it exists
 %  (e.g., when we are compiling on an ITO machine).
 %
-% Also, the papertype.inc files and rubric.inc files will be 
+% Also, the papertype.inc files and rubric.inc files will be
 %  loaded if we are on an ITO machine.  Otherwise, we will provide
 %  dummy mock-up values for those as well.
 %
@@ -501,7 +501,7 @@
 \newcommand\papertitle[1]{\global\def\nameofpaper{\uppercase{#1}}}
 \newcommand\papertype[1]{\global\def\typeofpaper{
  \InputIfFileExists{\itostatuspath #1}{}
-  { 
+  {
     %
     % If we're here, then this is running on exam preparer's
     % machine.  So, we will use mock-up values for the exam
@@ -556,11 +556,11 @@
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %
-% Now, we first see if we're on an ITO machine and can load the 
+% Now, we first see if we're on an ITO machine and can load the
 %  proper status.tex.  If so, we do it and execute the corresponding
-%  \coursestatusfcn.  
+%  \coursestatusfcn.
 %
-% Otherwise, based upon the value of courseid, we need to populate  
+% Otherwise, based upon the value of courseid, we need to populate
 %  the title and type with basic mock-up data.
 %
 % This command must be called in the top-level exam document, after
@@ -586,9 +586,9 @@
 
     \ifthenelse{\equal{\courseid}{anlp}}
       {\anlpdetails}{}
-    \ifthenelse{\equal{\courseid}{aleone}} 
+    \ifthenelse{\equal{\courseid}{aleone}}
       {\aleonedetails}{}
-	\ifthenelse{\equal{\courseid}{adbs}} 
+	\ifthenelse{\equal{\courseid}{adbs}}
       {\adbsdetails}{}
     \ifthenelse{\equal{\courseid}{av}}
       {\avdetails}{}
@@ -649,7 +649,7 @@
     \ifthenelse{\equal{\courseid}{dmmr}}
       {\dmmrdetails}{}
     \ifthenelse{\equal{\courseid}{dmr}}
-      {\dmrdetails}{}	  
+      {\dmrdetails}{}
     \ifthenelse{\equal{\courseid}{ds}}
       {\dsdetails}{}
 	\ifthenelse{\equal{\courseid}{epl}}
@@ -697,13 +697,13 @@
     \ifthenelse{\equal{\courseid}{imc}}
       {\imcdetails}{}
     \ifthenelse{\equal{\courseid}{iotssc}}
-      {\iotsscdetails}{}	  
+      {\iotsscdetails}{}
     \ifthenelse{\equal{\courseid}{iqc}}
       {\iqcdetails}{}
     \ifthenelse{\equal{\courseid}{itcs}}
       {\itcsdetails}{}
     \ifthenelse{\equal{\courseid}{ivc}}
-      {\ivcdetails}{}	  
+      {\ivcdetails}{}
     \ifthenelse{\equal{\courseid}{ivr}}
       {\ivrdetails}{}
     \ifthenelse{\equal{\courseid}{iaml}}
@@ -718,9 +718,9 @@
       {\mtdetails}{}
 	\ifthenelse{\equal{\courseid}{mi}}
 	  {\midetails}{}
-    \ifthenelse{\equal{\courseid}{nlu}} 
+    \ifthenelse{\equal{\courseid}{nlu}}
       {\nludetails}{}
-    \ifthenelse{\equal{\courseid}{nc}} 
+    \ifthenelse{\equal{\courseid}{nc}}
       {\ncdetails}{}
     \ifthenelse{\equal{\courseid}{nip}}
       {\nipdetails}{}
@@ -729,7 +729,7 @@
     \ifthenelse{\equal{\courseid}{pa}}
       {\padetails}{}
     \ifthenelse{\equal{\courseid}{pdiot}}
-      {\pdiotdetails}{}	  
+      {\pdiotdetails}{}
     \ifthenelse{\equal{\courseid}{ppls}}
       {\pplsdetails}{}
     \ifthenelse{\equal{\courseid}{pm}}
@@ -764,13 +764,13 @@
       {\tspldetails}{}
 
   }
-  { 
+  {
    %
    % If we're here, then we're on an exam preparer's machine.
    % So, we're going to use their set \courseid to give some
    %  nice mock-up values to the title and type text.
    %
-  
+
     \ifthenelse{\equal{\courseid}{anlp}}
       {\papertitle{INFR 11125 Accelerated Natural Language Processing}
        \papertype{msc.inc}}{}
@@ -866,7 +866,7 @@
        \papertype{inf3.inc}}{}
     \ifthenelse{\equal{\courseid}{dmr}}
       {\papertitle{Decision Making in Robots and Autonomous Agents}
-       \papertype{nonhons.inc}}{}	   
+       \papertype{nonhons.inc}}{}
     \ifthenelse{\equal{\courseid}{dmmr}}
       {\papertitle{Discrete Mathematics and Mathematical Reasoning}
        \papertype{nonhons.inc}}{}
@@ -950,7 +950,7 @@
         \papertype{inf3.inc}}{}
     \ifthenelse{\equal{\courseid}{ivc}}
       {\papertitle{Image and Vision Computing}
-       \papertype{msc.inc}}{}		
+       \papertype{msc.inc}}{}
     \ifthenelse{\equal{\courseid}{ivr}}
       {\papertitle{Introduction to Vision and Robotics}
        \papertype{inf3.inc}}{}
@@ -971,7 +971,7 @@
        \papertype{inf4.inc}}{}
     \ifthenelse{\equal{\courseid}{mi}}
       {\papertitle{INFR11079 Music Informatics}
-       \papertype{msc.inc}}{}	  
+       \papertype{msc.inc}}{}
     \ifthenelse{\equal{\courseid}{nlu}}
       {\papertitle{Natural Language Understanding (Level 11)}
        \papertype{inf4.inc}}{}
@@ -1046,7 +1046,7 @@
  % Let's also do a mock-up date/time to make the exam preparer happy:
  % (Aren't we sweet?)
  %
-  
+
     \paperdate{1}{4}{2017}
     \papertimes{00:00}{00:00}
 
@@ -1092,7 +1092,7 @@
  \ifthenelse{\equal{\rubricid}{custom}}{}
  {
      %% HONS RUBRICS
-     
+
      \ifthenelse{\equal{\rubricid}{qu1_and_either_qu2_or_qu3}}{
      \setrubrictype{
          Answer QUESTION 1 and ONE other question. \\
@@ -1103,7 +1103,7 @@
 	      \bigskip
 	     CALCULATORS MAY NOT BE USED IN THIS EXAMINATION \\
          }
-         
+
          %% Additional command to be used for question 1.
          \def\rubricqA{THIS QUESTION IS COMPULSORY}
 		 \def\rubricqB{ANSWER EITHER THIS QUESTION OR QUESTION 3}
@@ -1121,7 +1121,7 @@
 
          CALCULATORS MAY BE USED IN THIS EXAMINATION \\
          }
-         
+
          %% Additional command to be used for question 1.
          \def\rubricqA{THIS QUESTION IS COMPULSORY}
 		 \def\rubricqB{ANSWER EITHER THIS QUESTION OR QUESTION 3}
@@ -1147,7 +1147,7 @@
          CALCULATORS MAY BE USED IN THIS EXAMINATION \\
          }
      }{}
-       
+
      \ifthenelse{\equal{\rubricid}{infone}}{
      \setrubrictype{
 	     \begin{enumerate}
@@ -1181,7 +1181,7 @@
          \end{enumerate}
          }
      }{}
-	
+
  }
 }
 
@@ -1191,7 +1191,7 @@
 % Now, we can build the title page.  This command must be called
 %  from the top-level exam document.
 %
-% To do so: \examtitlepage 
+% To do so: \examtitlepage
 %
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
@@ -1244,5 +1244,3 @@ THIS EXAMINATION WILL BE MARKED ANONYMOUSLY
 
 \status
 }
-
-
diff --git a/tspl/tspl.agda-lib b/courses/puc/2019/puc2019.agda-lib
similarity index 100%
rename from tspl/tspl.agda-lib
rename to courses/puc/2019/puc2019.agda-lib
diff --git a/tspl/puc.md b/courses/puc/2019/puc2019.md
similarity index 79%
rename from tspl/puc.md
rename to courses/puc/2019/puc2019.md
index d23d11bf..42672415 100644
--- a/tspl/puc.md
+++ b/courses/puc/2019/puc2019.md
@@ -1,7 +1,7 @@
 ---
 title     : "PUC-Rio: Course notes"
 layout    : page
-permalink : /PUC/
+permalink : /PUC/2019/
 ---
 
 ## Staff
@@ -94,14 +94,14 @@ Lectures and tutorials take place Fridays and some Thursdays in 548L.
 
 For instructions on how to set up Agda for PLFA see [Getting Started](/GettingStarted/).
 
-* [PUC Assignment 1][PUC-Assignment1] due Friday 26 April.
-* [PUC Assignment 2][PUC-Assignment2] due Wednesday 22 May.
-* [PUC Assignment 3][PUC-Assignment3] due Wednesday 5 June.
-* [PUC Assignment 4][PUC-Assignment4] due Wednesday 19 June.
-* [PUC Assignment 5][PUC-Assignment5] due Tuesday 25 June.
-* [PUC Assignment 6](/tspl/first-mock.pdf) due Tuesday 25 June.
-  Use file [Exam][Exam]. Despite the rubric, do **all three questions**.
+* [PUC Assignment 1](/PUC/2019/Assignment1/) due Friday 26 April.
+* [PUC Assignment 2](/PUC/2019/Assignment2/) due Wednesday 22 May.
+* [PUC Assignment 3](/PUC/2019/Assignment3/) due Wednesday 5 June.
+* [PUC Assignment 4](/PUC/2019/Assignment4/) due Wednesday 19 June.
+* [PUC Assignment 5](/PUC/2019/Assignment5/) due Tuesday 25 June.
+* [PUC Assignment 6](/courses/tspl/2018/Mock1.pdf) due Tuesday 25 June.
+  Use file [Exam](/PUC/2019/Exam/). Despite the rubric, do **all three questions**.
 
 Submit assignments by email to [wadler@inf.ed.ac.uk](mailto:wadler@inf.ed.ac.uk).
-Attach a single file named `PUC-Assignment1.lagda` or the like.  Include
+Attach a single file named `Assignment1.lagda.md` or the like.  Include
 your name and email in the submitted file.
diff --git a/tspl/Assignment1.lagda.md b/courses/tspl/2018/Assignment1.lagda.md
similarity index 98%
rename from tspl/Assignment1.lagda.md
rename to courses/tspl/2018/Assignment1.lagda.md
index 565c7bc9..de5c4014 100644
--- a/tspl/Assignment1.lagda.md
+++ b/courses/tspl/2018/Assignment1.lagda.md
@@ -1,7 +1,7 @@
 ---
 title     : "Assignment1: TSPL Assignment 1"
 layout    : page
-permalink : /Assignment1/
+permalink : /TSPL/2018/Assignment1/
 ---
 
 ```
@@ -125,7 +125,7 @@ Give an example of an operator that has an identity and is
 associative but is not commutative.
 
 
-#### Exercise `finite-+-assoc` (stretch) {#finite-plus-assoc}
+#### Exercise `finite-|-assoc` (stretch) {#finite-plus-assoc}
 
 Write out what is known about associativity of addition on each of the first four
 days using a finite story of creation, as
@@ -179,7 +179,7 @@ Show
 
 for all naturals `n`. Did your proof require induction?
 
-#### Exercise `∸-+-assoc` {#monus-plus-assoc}
+#### Exercise `∸-|-assoc` {#monus-plus-assoc}
 
 Show that monus associates with addition, that is,
 
diff --git a/tspl/Assignment2.lagda.md b/courses/tspl/2018/Assignment2.lagda.md
similarity index 99%
rename from tspl/Assignment2.lagda.md
rename to courses/tspl/2018/Assignment2.lagda.md
index 35f2028d..9d75e28c 100644
--- a/tspl/Assignment2.lagda.md
+++ b/courses/tspl/2018/Assignment2.lagda.md
@@ -1,7 +1,7 @@
 ---
 title     : "Assignment2: TSPL Assignment 2"
 layout    : page
-permalink : /Assignment2/
+permalink : /TSPL/2018/Assignment2/
 ---
 
 ```
diff --git a/tspl/Assignment3.lagda.md b/courses/tspl/2018/Assignment3.lagda.md
similarity index 99%
rename from tspl/Assignment3.lagda.md
rename to courses/tspl/2018/Assignment3.lagda.md
index 651c83eb..51c9d8ae 100644
--- a/tspl/Assignment3.lagda.md
+++ b/courses/tspl/2018/Assignment3.lagda.md
@@ -1,7 +1,7 @@
 ---
 title     : "Assignment3: TSPL Assignment 3"
 layout    : page
-permalink : /Assignment3/
+permalink : /TSPL/2018/Assignment3/
 ---
 
 ```
diff --git a/tspl/Assignment4.lagda.md b/courses/tspl/2018/Assignment4.lagda.md
similarity index 99%
rename from tspl/Assignment4.lagda.md
rename to courses/tspl/2018/Assignment4.lagda.md
index 3a1c7b9f..f5fb3774 100644
--- a/tspl/Assignment4.lagda.md
+++ b/courses/tspl/2018/Assignment4.lagda.md
@@ -1,7 +1,7 @@
 ---
 title     : "Assignment4: TSPL Assignment 4"
 layout    : page
-permalink : /Assignment4/
+permalink : /TSPL/2018/Assignment4/
 ---
 
 ```
diff --git a/courses/tspl/2018/Exam.lagda.md b/courses/tspl/2018/Exam.lagda.md
new file mode 100644
index 00000000..c90d1046
--- /dev/null
+++ b/courses/tspl/2018/Exam.lagda.md
@@ -0,0 +1,678 @@
+---
+title     : "Exam: TSPL Mock Exam file"
+layout    : page
+permalink : /TSPL/2018/Exam/
+---
+
+
+```
+module Exam where
+```
+
+**IMPORTANT** For ease of marking, when modifying the given code please write
+
+    -- begin
+    -- end
+
+before and after code you add, to indicate your changes.
+
+## Imports
+
+```
+import Relation.Binary.PropositionalEquality as Eq
+open Eq using (_≡_; refl; sym; trans; cong; _≢_)
+open import Data.Empty using (⊥; ⊥-elim)
+open import Data.Nat using (ℕ; zero; suc)
+open import Data.List using (List; []; _∷_; _++_)
+open import Data.Product using (∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
+open import Data.String using (String; _≟_)
+open import Relation.Nullary using (¬_; Dec; yes; no)
+open import Relation.Binary using (Decidable)
+```
+
+## Problem 1
+
+```
+module Problem1 where
+
+  open import Function using (_∘_)
+```
+
+Remember to indent all code by two spaces.
+
+### (a)
+
+### (b)
+
+### (c)
+
+
+## Problem 2
+
+Remember to indent all code by two spaces.
+
+```
+module Problem2 where
+```
+
+### Infix declarations
+
+```
+  infix  4 _⊢_
+  infix  4 _∋_
+  infixl 5 _,_
+
+  infixr 7 _⇒_
+
+  infix  5 ƛ_
+  infix  5 μ_
+  infixl 7 _·_
+  infix  8 `suc_
+  infix  9 `_
+  infix  9 S_
+  infix  9 #_
+```
+
+### Types and contexts
+
+```
+  data Type : Set where
+    _⇒_   : Type → Type → Type
+    `ℕ    : Type
+
+  data Context : Set where
+    ∅   : Context
+    _,_ : Context → Type → Context
+```
+
+### Variables and the lookup judgment
+
+```
+  data _∋_ : Context → Type → Set where
+
+    Z : ∀ {Γ A}
+        ----------
+      → Γ , A ∋ A
+
+    S_ : ∀ {Γ A B}
+      → Γ ∋ A
+        ---------
+      → Γ , B ∋ A
+```
+
+### Terms and the typing judgment
+
+```
+  data _⊢_ : Context → Type → Set where
+
+    `_ : ∀ {Γ} {A}
+      → Γ ∋ A
+        ------
+      → Γ ⊢ A
+
+    ƛ_  :  ∀ {Γ} {A B}
+      → Γ , A ⊢ B
+        ----------
+      → Γ ⊢ A ⇒ B
+
+    _·_ : ∀ {Γ} {A B}
+      → Γ ⊢ A ⇒ B
+      → Γ ⊢ A
+        ----------
+      → Γ ⊢ B
+
+    `zero : ∀ {Γ}
+        ----------
+      → Γ ⊢ `ℕ
+
+    `suc_ : ∀ {Γ}
+      → Γ ⊢ `ℕ
+        -------
+      → Γ ⊢ `ℕ
+
+    case : ∀ {Γ A}
+      → Γ ⊢ `ℕ
+      → Γ ⊢ A
+      → Γ , `ℕ ⊢ A
+        -----------
+      → Γ ⊢ A
+
+    μ_ : ∀ {Γ A}
+      → Γ , A ⊢ A
+        ----------
+      → Γ ⊢ A
+```
+
+### Abbreviating de Bruijn indices
+
+```
+  lookup : Context → ℕ → Type
+  lookup (Γ , A) zero     =  A
+  lookup (Γ , _) (suc n)  =  lookup Γ n
+  lookup ∅       _        =  ⊥-elim impossible
+    where postulate impossible : ⊥
+
+  count : ∀ {Γ} → (n : ℕ) → Γ ∋ lookup Γ n
+  count {Γ , _} zero     =  Z
+  count {Γ , _} (suc n)  =  S (count n)
+  count {∅}     _        =  ⊥-elim impossible
+    where postulate impossible : ⊥
+
+  #_ : ∀ {Γ} → (n : ℕ) → Γ ⊢ lookup Γ n
+  # n  =  ` count n
+```
+
+### Renaming
+
+```
+  ext : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A)
+      -----------------------------------
+    → (∀ {A B} → Γ , B ∋ A → Δ , B ∋ A)
+  ext ρ Z      =  Z
+  ext ρ (S x)  =  S (ρ x)
+
+  rename : ∀ {Γ Δ}
+    → (∀ {A} → Γ ∋ A → Δ ∋ A)
+      ------------------------
+    → (∀ {A} → Γ ⊢ A → Δ ⊢ A)
+  rename ρ (` x)          =  ` (ρ x)
+  rename ρ (ƛ N)          =  ƛ (rename (ext ρ) N)
+  rename ρ (L · M)        =  (rename ρ L) · (rename ρ M)
+  rename ρ (`zero)        =  `zero
+  rename ρ (`suc M)       =  `suc (rename ρ M)
+  rename ρ (case L M N)   =  case (rename ρ L) (rename ρ M) (rename (ext ρ) N)
+  rename ρ (μ N)          =  μ (rename (ext ρ) N)
+```
+
+### Simultaneous Substitution
+
+```
+  exts : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ⊢ A)
+      ----------------------------------
+    → (∀ {A B} → Γ , B ∋ A → Δ , B ⊢ A)
+  exts σ Z      =  ` Z
+  exts σ (S x)  =  rename S_ (σ x)
+
+  subst : ∀ {Γ Δ}
+    → (∀ {A} → Γ ∋ A → Δ ⊢ A)
+      ------------------------
+    → (∀ {A} → Γ ⊢ A → Δ ⊢ A)
+  subst σ (` k)          =  σ k
+  subst σ (ƛ N)          =  ƛ (subst (exts σ) N)
+  subst σ (L · M)        =  (subst σ L) · (subst σ M)
+  subst σ (`zero)        =  `zero
+  subst σ (`suc M)       =  `suc (subst σ M)
+  subst σ (case L M N)   =  case (subst σ L) (subst σ M) (subst (exts σ) N)
+  subst σ (μ N)          =  μ (subst (exts σ) N)
+```
+
+### Single substitution
+
+```
+  _[_] : ∀ {Γ A B}
+          → Γ , B ⊢ A
+          → Γ ⊢ B
+            ---------
+          → Γ ⊢ A
+  _[_] {Γ} {A} {B} N M =  subst {Γ , B} {Γ} σ {A} N
+    where
+    σ : ∀ {A} → Γ , B ∋ A → Γ ⊢ A
+    σ Z      =  M
+    σ (S x)  =  ` x
+```
+
+### Values
+
+```
+  data Value : ∀ {Γ A} → Γ ⊢ A → Set where
+
+    V-ƛ : ∀ {Γ A B} {N : Γ , A ⊢ B}
+        ---------------------------
+      → Value (ƛ N)
+
+    V-zero : ∀ {Γ}
+        -----------------
+      → Value (`zero {Γ})
+
+    V-suc : ∀ {Γ} {V : Γ ⊢ `ℕ}
+      → Value V
+        --------------
+      → Value (`suc V)
+```
+
+### Reduction
+
+```
+  infix 2 _—→_
+
+  data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
+
+    ξ-·₁ : ∀ {Γ A B} {L L′ : Γ ⊢ A ⇒ B} {M : Γ ⊢ A}
+      → L —→ L′
+        -----------------
+      → L · M —→ L′ · M
+
+    ξ-·₂ : ∀ {Γ A B} {V : Γ ⊢ A ⇒ B} {M M′ : Γ ⊢ A}
+      → Value V
+      → M —→ M′
+        --------------
+      → V · M —→ V · M′
+
+    β-ƛ : ∀ {Γ A B} {N : Γ , A ⊢ B} {W : Γ ⊢ A}
+      → Value W
+        -------------------
+      → (ƛ N) · W —→ N [ W ]
+
+    ξ-suc : ∀ {Γ} {M M′ : Γ ⊢ `ℕ}
+      → M —→ M′
+        ----------------
+      → `suc M —→ `suc M′
+
+    ξ-case : ∀ {Γ A} {L L′ : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
+      → L —→ L′
+        --------------------------
+      → case L M N —→ case L′ M N
+
+    β-zero :  ∀ {Γ A} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
+        -------------------
+      → case `zero M N —→ M
+
+    β-suc : ∀ {Γ A} {V : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
+      → Value V
+        -----------------------------
+      → case (`suc V) M N —→ N [ V ]
+
+    β-μ : ∀ {Γ A} {N : Γ , A ⊢ A}
+        ---------------
+      → μ N —→ N [ μ N ]
+```
+
+
+### Reflexive and transitive closure
+
+```
+  infix  2 _—↠_
+  infix  1 begin_
+  infixr 2 _—→⟨_⟩_
+  infix  3 _∎
+
+  data _—↠_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
+
+    _∎ : ∀ {Γ A} (M : Γ ⊢ A)
+        --------
+      → M —↠ M
+
+    _—→⟨_⟩_ : ∀ {Γ A} (L : Γ ⊢ A) {M N : Γ ⊢ A}
+      → L —→ M
+      → M —↠ N
+        ---------
+      → L —↠ N
+
+  begin_ : ∀ {Γ} {A} {M N : Γ ⊢ A}
+    → M —↠ N
+      ------
+    → M —↠ N
+  begin M—↠N = M—↠N
+```
+
+
+### Progress
+
+```
+  data Progress {A} (M : ∅ ⊢ A) : Set where
+
+    step : ∀ {N : ∅ ⊢ A}
+      → M —→ N
+        -------------
+      → Progress M
+
+    done :
+        Value M
+        ----------
+      → Progress M
+
+  progress : ∀ {A} → (M : ∅ ⊢ A) → Progress M
+  progress (` ())
+  progress (ƛ N)                          =  done V-ƛ
+  progress (L · M) with progress L
+  ...    | step L—→L′                     =  step (ξ-·₁ L—→L′)
+  ...    | done V-ƛ with progress M
+  ...        | step M—→M′                 =  step (ξ-·₂ V-ƛ M—→M′)
+  ...        | done VM                    =  step (β-ƛ VM)
+  progress (`zero)                        =  done V-zero
+  progress (`suc M) with progress M
+  ...    | step M—→M′                     =  step (ξ-suc M—→M′)
+  ...    | done VM                        =  done (V-suc VM)
+  progress (case L M N) with progress L
+  ...    | step L—→L′                     =  step (ξ-case L—→L′)
+  ...    | done V-zero                    =  step (β-zero)
+  ...    | done (V-suc VL)                =  step (β-suc VL)
+  progress (μ N)                          =  step (β-μ)
+```
+
+### Evaluation
+
+```
+  data Gas : Set where
+    gas : ℕ → Gas
+
+  data Finished {Γ A} (N : Γ ⊢ A) : Set where
+
+     done :
+         Value N
+         ----------
+       → Finished N
+
+     out-of-gas :
+         ----------
+         Finished N
+
+  data Steps : ∀ {A} → ∅ ⊢ A → Set where
+
+    steps : ∀ {A} {L N : ∅ ⊢ A}
+      → L —↠ N
+      → Finished N
+        ----------
+      → Steps L
+
+  eval : ∀ {A}
+    → Gas
+    → (L : ∅ ⊢ A)
+      -----------
+    → Steps L
+  eval (gas zero)    L                     =  steps (L ∎) out-of-gas
+  eval (gas (suc m)) L with progress L
+  ... | done VL                            =  steps (L ∎) (done VL)
+  ... | step {M} L—→M with eval (gas m) M
+  ...    | steps M—↠N fin                  =  steps (L —→⟨ L—→M ⟩ M—↠N) fin
+```
+
+## Problem 3
+
+Remember to indent all code by two spaces.
+
+```
+module Problem3 where
+```
+
+### Imports
+
+```
+  import plfa.DeBruijn as DB
+```
+
+### Syntax
+
+```
+  infix   4  _∋_⦂_
+  infix   4  _⊢_↑_
+  infix   4  _⊢_↓_
+  infixl  5  _,_⦂_
+
+  infix   5  ƛ_⇒_
+  infix   5  μ_⇒_
+  infix   6  _↑
+  infix   6  _↓_
+  infixl  7  _·_
+  infix   8  `suc_
+  infix   9  `_
+```
+
+### Types
+
+```
+  data Type : Set where
+    _⇒_   : Type → Type → Type
+    `ℕ    : Type
+```
+
+### Identifiers
+
+```
+  Id : Set
+  Id = String
+```
+
+### Contexts
+
+```
+  data Context : Set where
+    ∅     : Context
+    _,_⦂_ : Context → Id → Type → Context
+```
+
+### Terms
+
+```
+  data Term⁺ : Set
+  data Term⁻ : Set
+
+  data Term⁺ where
+    `_                        : Id → Term⁺
+    _·_                       : Term⁺ → Term⁻ → Term⁺
+    _↓_                       : Term⁻ → Type → Term⁺
+
+  data Term⁻ where
+    ƛ_⇒_                     : Id → Term⁻ → Term⁻
+    `zero                    : Term⁻
+    `suc_                    : Term⁻ → Term⁻
+    `case_[zero⇒_|suc_⇒_]    : Term⁺ → Term⁻ → Id → Term⁻ → Term⁻
+    μ_⇒_                     : Id → Term⁻ → Term⁻
+    _↑                       : Term⁺ → Term⁻
+```
+
+### Lookup
+
+```
+  data _∋_⦂_ : Context → Id → Type → Set where
+
+    Z : ∀ {Γ x A}
+        --------------------
+      → Γ , x ⦂ A ∋ x ⦂ A
+
+    S : ∀ {Γ x y A B}
+      → x ≢ y
+      → Γ ∋ x ⦂ A
+        -----------------
+      → Γ , y ⦂ B ∋ x ⦂ A
+```
+
+### Bidirectional type checking
+
+```
+  data _⊢_↑_ : Context → Term⁺ → Type → Set
+  data _⊢_↓_ : Context → Term⁻ → Type → Set
+
+  data _⊢_↑_ where
+
+    ⊢` : ∀ {Γ A x}
+      → Γ ∋ x ⦂ A
+        -----------
+      → Γ ⊢ ` x ↑ A
+
+    _·_ : ∀ {Γ L M A B}
+      → Γ ⊢ L ↑ A ⇒ B
+      → Γ ⊢ M ↓ A
+        -------------
+      → Γ ⊢ L · M ↑ B
+
+    ⊢↓ : ∀ {Γ M A}
+      → Γ ⊢ M ↓ A
+        ---------------
+      → Γ ⊢ (M ↓ A) ↑ A
+
+  data _⊢_↓_ where
+
+    ⊢ƛ : ∀ {Γ x N A B}
+      → Γ , x ⦂ A ⊢ N ↓ B
+        -------------------
+      → Γ ⊢ ƛ x ⇒ N ↓ A ⇒ B
+
+    ⊢zero : ∀ {Γ}
+        --------------
+      → Γ ⊢ `zero ↓ `ℕ
+
+    ⊢suc : ∀ {Γ M}
+      → Γ ⊢ M ↓ `ℕ
+        ---------------
+      → Γ ⊢ `suc M ↓ `ℕ
+
+    ⊢case : ∀ {Γ L M x N A}
+      → Γ ⊢ L ↑ `ℕ
+      → Γ ⊢ M ↓ A
+      → Γ , x ⦂ `ℕ ⊢ N ↓ A
+        -------------------------------------
+      → Γ ⊢ `case L [zero⇒ M |suc x ⇒ N ] ↓ A
+
+    ⊢μ : ∀ {Γ x N A}
+      → Γ , x ⦂ A ⊢ N ↓ A
+        -----------------
+      → Γ ⊢ μ x ⇒ N ↓ A
+
+    ⊢↑ : ∀ {Γ M A B}
+      → Γ ⊢ M ↑ A
+      → A ≡ B
+        -------------
+      → Γ ⊢ (M ↑) ↓ B
+```
+
+
+### Type equality
+
+```
+  _≟Tp_ : (A B : Type) → Dec (A ≡ B)
+  `ℕ      ≟Tp `ℕ              =  yes refl
+  `ℕ      ≟Tp (A ⇒ B)         =  no λ()
+  (A ⇒ B) ≟Tp `ℕ              =  no λ()
+  (A ⇒ B) ≟Tp (A′ ⇒ B′)
+    with A ≟Tp A′ | B ≟Tp B′
+  ...  | no A≢    | _         =  no λ{refl → A≢ refl}
+  ...  | yes _    | no B≢     =  no λ{refl → B≢ refl}
+  ...  | yes refl | yes refl  =  yes refl
+```
+
+### Prerequisites
+
+```
+  dom≡ : ∀ {A A′ B B′} → A ⇒ B ≡ A′ ⇒ B′ → A ≡ A′
+  dom≡ refl = refl
+
+  rng≡ : ∀ {A A′ B B′} → A ⇒ B ≡ A′ ⇒ B′ → B ≡ B′
+  rng≡ refl = refl
+
+  ℕ≢⇒ : ∀ {A B} → `ℕ ≢ A ⇒ B
+  ℕ≢⇒ ()
+```
+
+
+### Unique lookup
+
+```
+  uniq-∋ : ∀ {Γ x A B} → Γ ∋ x ⦂ A → Γ ∋ x ⦂ B → A ≡ B
+  uniq-∋ Z Z                 =  refl
+  uniq-∋ Z (S x≢y _)         =  ⊥-elim (x≢y refl)
+  uniq-∋ (S x≢y _) Z         =  ⊥-elim (x≢y refl)
+  uniq-∋ (S _ ∋x) (S _ ∋x′)  =  uniq-∋ ∋x ∋x′
+```
+
+### Unique synthesis
+
+```
+  uniq-↑ : ∀ {Γ M A B} → Γ ⊢ M ↑ A → Γ ⊢ M ↑ B → A ≡ B
+  uniq-↑ (⊢` ∋x) (⊢` ∋x′)       =  uniq-∋ ∋x ∋x′
+  uniq-↑ (⊢L · ⊢M) (⊢L′ · ⊢M′)  =  rng≡ (uniq-↑ ⊢L ⊢L′)
+  uniq-↑ (⊢↓ ⊢M) (⊢↓ ⊢M′)       =  refl
+```
+
+## Lookup type of a variable in the context
+
+```
+  ext∋ : ∀ {Γ B x y}
+    → x ≢ y
+    → ¬ ∃[ A ]( Γ ∋ x ⦂ A )
+      -----------------------------
+    → ¬ ∃[ A ]( Γ , y ⦂ B ∋ x ⦂ A )
+  ext∋ x≢y _  ⟨ A , Z ⟩       =  x≢y refl
+  ext∋ _   ¬∃ ⟨ A , S _ ⊢x ⟩  =  ¬∃ ⟨ A , ⊢x ⟩
+
+  lookup : ∀ (Γ : Context) (x : Id)
+      -----------------------
+    → Dec (∃[ A ](Γ ∋ x ⦂ A))
+  lookup ∅ x                        =  no  (λ ())
+  lookup (Γ , y ⦂ B) x with x ≟ y
+  ... | yes refl                    =  yes ⟨ B , Z ⟩
+  ... | no x≢y with lookup Γ x
+  ...             | no  ¬∃          =  no  (ext∋ x≢y ¬∃)
+  ...             | yes ⟨ A , ⊢x ⟩  =  yes ⟨ A , S x≢y ⊢x ⟩
+```
+
+### Promoting negations
+
+```
+  ¬arg : ∀ {Γ A B L M}
+    → Γ ⊢ L ↑ A ⇒ B
+    → ¬ Γ ⊢ M ↓ A
+      -------------------------
+    → ¬ ∃[ B′ ](Γ ⊢ L · M ↑ B′)
+  ¬arg ⊢L ¬⊢M ⟨ B′ , ⊢L′ · ⊢M′ ⟩ rewrite dom≡ (uniq-↑ ⊢L ⊢L′) = ¬⊢M ⊢M′
+
+  ¬switch : ∀ {Γ M A B}
+    → Γ ⊢ M ↑ A
+    → A ≢ B
+      ---------------
+    → ¬ Γ ⊢ (M ↑) ↓ B
+  ¬switch ⊢M A≢B (⊢↑ ⊢M′ A′≡B) rewrite uniq-↑ ⊢M ⊢M′ = A≢B A′≡B
+```
+
+
+## Synthesize and inherit types
+
+```
+  synthesize : ∀ (Γ : Context) (M : Term⁺)
+      -----------------------
+    → Dec (∃[ A ](Γ ⊢ M ↑ A))
+
+  inherit : ∀ (Γ : Context) (M : Term⁻) (A : Type)
+      ---------------
+    → Dec (Γ ⊢ M ↓ A)
+
+  synthesize Γ (` x) with lookup Γ x
+  ... | no  ¬∃              =  no  (λ{ ⟨ A , ⊢` ∋x ⟩ → ¬∃ ⟨ A , ∋x ⟩ })
+  ... | yes ⟨ A , ∋x ⟩      =  yes ⟨ A , ⊢` ∋x ⟩
+  synthesize Γ (L · M) with synthesize Γ L
+  ... | no  ¬∃              =  no  (λ{ ⟨ _ , ⊢L  · _  ⟩  →  ¬∃ ⟨ _ , ⊢L ⟩ })
+  ... | yes ⟨ `ℕ ,    ⊢L ⟩  =  no  (λ{ ⟨ _ , ⊢L′ · _  ⟩  →  ℕ≢⇒ (uniq-↑ ⊢L ⊢L′) })
+  ... | yes ⟨ A ⇒ B , ⊢L ⟩ with inherit Γ M A
+  ...    | no  ¬⊢M          =  no  (¬arg ⊢L ¬⊢M)
+  ...    | yes ⊢M           =  yes ⟨ B , ⊢L · ⊢M ⟩
+  synthesize Γ (M ↓ A) with inherit Γ M A
+  ... | no  ¬⊢M             =  no  (λ{ ⟨ _ , ⊢↓ ⊢M ⟩  →  ¬⊢M ⊢M })
+  ... | yes ⊢M              =  yes ⟨ A , ⊢↓ ⊢M ⟩
+
+  inherit Γ (ƛ x ⇒ N) `ℕ      =  no  (λ())
+  inherit Γ (ƛ x ⇒ N) (A ⇒ B) with inherit (Γ , x ⦂ A) N B
+  ... | no ¬⊢N                =  no  (λ{ (⊢ƛ ⊢N)  →  ¬⊢N ⊢N })
+  ... | yes ⊢N                =  yes (⊢ƛ ⊢N)
+  inherit Γ `zero `ℕ          =  yes ⊢zero
+  inherit Γ `zero (A ⇒ B)     =  no  (λ())
+  inherit Γ (`suc M) `ℕ with inherit Γ M `ℕ
+  ... | no ¬⊢M                =  no  (λ{ (⊢suc ⊢M)  →  ¬⊢M ⊢M })
+  ... | yes ⊢M                =  yes (⊢suc ⊢M)
+  inherit Γ (`suc M) (A ⇒ B)  =  no  (λ())
+  inherit Γ (`case L [zero⇒ M |suc x ⇒ N ]) A with synthesize Γ L
+  ... | no ¬∃                 =  no  (λ{ (⊢case ⊢L  _ _) → ¬∃ ⟨ `ℕ , ⊢L ⟩})
+  ... | yes ⟨ _ ⇒ _ , ⊢L ⟩    =  no  (λ{ (⊢case ⊢L′ _ _) → ℕ≢⇒ (uniq-↑ ⊢L′ ⊢L) })
+  ... | yes ⟨ `ℕ ,    ⊢L ⟩ with inherit Γ M A
+  ...    | no ¬⊢M             =  no  (λ{ (⊢case _ ⊢M _) → ¬⊢M ⊢M })
+  ...    | yes ⊢M with inherit (Γ , x ⦂ `ℕ) N A
+  ...       | no ¬⊢N          =  no  (λ{ (⊢case _ _ ⊢N) → ¬⊢N ⊢N })
+  ...       | yes ⊢N          =  yes (⊢case ⊢L ⊢M ⊢N)
+  inherit Γ (μ x ⇒ N) A with inherit (Γ , x ⦂ A) N A
+  ... | no ¬⊢N                =  no  (λ{ (⊢μ ⊢N) → ¬⊢N ⊢N })
+  ... | yes ⊢N                =  yes (⊢μ ⊢N)
+  inherit Γ (M ↑) B with synthesize Γ M
+  ... | no  ¬∃                =  no  (λ{ (⊢↑ ⊢M _) → ¬∃ ⟨ _ , ⊢M ⟩ })
+  ... | yes ⟨ A , ⊢M ⟩ with A ≟Tp B
+  ...   | no  A≢B             =  no  (¬switch ⊢M A≢B)
+  ...   | yes A≡B             =  yes (⊢↑ ⊢M A≡B)
+```
diff --git a/courses/tspl/2018/Instructions.tex b/courses/tspl/2018/Instructions.tex
new file mode 100644
index 00000000..8e845dd9
--- /dev/null
+++ b/courses/tspl/2018/Instructions.tex
@@ -0,0 +1,122 @@
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Instructions for TSPL Exam
+% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\documentclass[12pt]{article}
+\usepackage{a4,amssymb}
+% \setlength{\oddsidemargin}{-1.5cm}
+% \addtolength{\textwidth}{2cm}
+% \addtolength{\textheight}{3cm}
+
+\begin{document}
+\pagestyle{empty}
+\setcounter{page}{1}
+
+\begin{center}
+\large Types and Semantics for Programming Languages
+\end{center}
+
+\section*{Instructions}
+
+\begin{enumerate}
+
+\item
+  The exam lasts two hours.
+
+\item
+  Place your student identity card face-up on the desk in front of you.  The
+  invigilator may come to check your identity, and in this case you may be asked
+  to allow the invigilator to briefly use your computer.  The exam time has been
+  calculated to allow time for such interruptions.
+
+\item
+  You may log into your computer as soon as you are ready to do so.
+
+\item
+  To download the exam paper, open a terminal window and type:
+  \begin{center}
+    \texttt{getpapers}
+  \end{center}
+  This will create a subdirectory \texttt{tspl-pe} in your home directory,
+  containing the following files.
+  \begin{center}
+    \begin{tabular}{ll}
+      \texttt{tspl-pe/papers/exam.pdf}                & the exam \\
+      \texttt{tspl-pe/papers/instructions.pdf}        & these instructions \\
+      \texttt{tspl-pe/templates/Exam.lagda}           & exam template to edit \\
+      \texttt{tspl-pe/original\_templates/Exam.lagda} & backup of exam template
+    \end{tabular}
+  \end{center}
+  The directories \texttt{tspl-pe/papers} and
+  \texttt{tspl-pe/original\_templates}
+  are read only, but you may read and write \texttt{tspl-pe/templates}.
+
+\item
+  To setup the Agda environment, open a second terminal window and type:
+  \begin{center}
+    \texttt{tspl-setup}
+  \end{center}
+  This will open a browser, with three tabs which contain the textbook
+  \emph{Programming Language Foundations in Agda}, the documentation for the
+  Agda standard library, and the documentation for Agda.  (The browser may
+  also attempt to link to the internet, which brings up a tab labeled
+  ``Problem loading page''; this is expected and not a problem.)
+
+{\it (Note that internet access has been disabled.)}
+
+\begin{center}
+  \textbf{Do nothing further until the start of the exam is announced!}
+\end{center}
+
+\hfill \textit{Please Turn Over}
+\newpage
+
+\item When the start of the exam is announced, open the exam paper
+\begin{center}
+  \texttt{tspl-pe/papers/exam.pdf}
+\end{center}
+with the standard PDF viewer.
+
+\item Change to the template directory
+\begin{center}
+  \texttt{cd tspl-pe/templates}
+\end{center}
+and edit the file
+\begin{center}
+  \texttt{Exam.lagda}
+\end{center}
+to include your answers, using Emacs or anything else suitable.
+You are recommended to save your work on a regular basis.
+
+\item Before submitting, make sure your file is processed by Agda
+  correctly. Code which prevents the file from compiling should be
+  made into comments. If you fail to solve part of a problem, you
+  may get more credit if you indicate clearly which part you have
+  not solved.
+
+\item \emph{Please ensure before submission that the file}
+  \texttt{Exam.lagda} \emph{contains your solutions to the exam.}  Submit
+  your file using the command:
+  \begin{center}
+  \texttt{examsubmit Exam.lagda}
+  \end{center}
+  If you get an error, please check carefully that your file is called
+  \texttt{Exam.lagda} and that you are in the same directory as this
+  file. If you continue to have problems, please contact one of the
+  invigilators.
+
+Repeated submit commands are allowed, and will overwrite previous
+submissions.  The last file submitted will be the one marked.
+
+\item When the invigilators announce the end of the exam, you must
+  submit and log out immediately.
+
+\end{enumerate}
+
+\end{document}
+
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
diff --git a/courses/tspl/2018/Mock1.tex b/courses/tspl/2018/Mock1.tex
new file mode 100644
index 00000000..7991fc42
--- /dev/null
+++ b/courses/tspl/2018/Mock1.tex
@@ -0,0 +1,421 @@
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% I N F O R M A T I C S
+%  Honours Exam LaTeX Template for Exam Authors
+%
+%  Created: 12-Oct-2009 by G.O.Passmore.
+%  Last Updated: 10-Sep-2018 by I. Murray
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%% The following define the status of the exam papers in the order
+%%% required.  Simply remove the comment (i.e., the % symbol) just
+%%% before the appropriate one and comment the others out.
+
+%\newcommand\status{\internal}
+%\newcommand\status{\external}
+\newcommand\status{\final}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%% The following three lines are always required.  You may add
+%%% custom packages to the one already defined if necessary.
+
+\documentclass{examhons2018}
+\usepackage{amssymb}
+\usepackage{amsmath}
+\usepackage{semantic}
+\usepackage{stix}
+
+%%% Uncomment the \checkmarksfalse line if the macros that check the
+%%% mark totals cause problems. However, please do not make your
+%%% questions add up to a non-standard number of marks without
+%%% permission of the convenor.
+%\checkmarksfalse
+
+\begin{document}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Replace {ad} below with the ITO code for your course.  This will
+%  be used by the ITO LaTeX installation to install course-specific
+%  data into the exam versions it produces from this document.
+%
+% Your choices are (in course title order):
+%
+%   {anlp}     - Acc. Natural Language Processing	            (MSc)
+%   {aleone}   - Adaptive Learning Environments 1              (Inf4)
+%   {adbs}     - Advanced Databases                            (Inf4)
+%   {av}       - Advanced Vision                               (Inf4)
+%   {av-dl}    - Advanced Vision - distance learning            (MSc)
+%   {apl}      - Advances in Programming Languages             (Inf4)
+%   {abs}      - Agent Based Systems [L10]                     (Inf3)
+%   {afds}     - Algorithmic Foundations of Data Science        (MSc)
+%   {agta}     - Algorithmic Game Theory and its Apps.          (MSc)
+%   {ads}      - Algorithms and Data Structures                (Inf3)
+%   {ad}       - Applied Databases                              (MSc)
+%   {aipf}     - Artificial Intelligence Present and Future     (MSc)
+%   {ar}       - Automated Reasoning 	                       (Inf3)
+%   {asr}      - Automatic Speech Recognition                  (Inf4)
+%   {bioone}   - Bioinformatics 1                               (MSc)
+%   {biotwo}   - Bioinformatics 2                               (MSc)
+%	{bdl}      - Blockchains and Distributed Ledgers		   (Inf4)
+%   {cqi}      - Categories and Quantum Informatics             (MSc)
+%   {copt}     - Compiler Opimisation [L11]                    (Inf4)
+%   {ct}       - Compiling Techniques                          (Inf3)
+%   {ccs}      - Computational Cognitive Science               (Inf3)
+%   {cmc}      - Computational Complexity                      (Inf4)
+%   {ca}       - Computer Algebra                              (Inf4)
+%   {cav}      - Computer Animation and Visualisation          (Inf4)
+%   {car}      - Computer Architecture                         (Inf3)
+%   {comn}     - Computer Comms. and Networks                  (Inf3)
+%   {cd}       - Computer Design                               (Inf3)
+%   {cg}       - Computer Graphics [L11]                       (Inf4)
+%   {cn}       - Computer Networking [L11]                     (Inf4)
+%   {cp}       - Computer Prog. Skills and Concepts         (nonhons)
+%   {cs}       - Computer Security                             (Inf3)
+%   {dds}      - Data, Design and Society                   (nonhons)
+%   {dme}      - Data Mining and Exploration                   (Msc)
+%   {dbs}      - Database Systems                              (Inf3)
+%   {dmr}      - Decision Making in Robots and Autonomous Agents(MSc)
+%   {dmmr}     - Discrete Maths. and Math. Reasoning        (nonhons)
+%   {ds}       - Distributed Systems [L11]                     (Inf4)
+%   {epl}      - Elements of Programming Languages             (Inf3)
+%   {es}       - Embedded Software                             (Inf4)
+%   {exc}      - Extreme Computing                             (Inf4)
+%   {fv}       - Formal Verification                           (Inf4)
+%   {fnlp}     - Foundations of Natural Language Processing    (Inf3)
+%   {hci}      - Human-Computer Interaction [L11]              (Inf4)
+%   {infonea}  - Informatics 1 - Introduction to Computation(nonhons)
+%   different sittings for INF1A programming exams
+%   {infoneapone}  - Informatics 1 - Introduction to Computation(nonhons)
+%   {infoneaptwo}  - Informatics 1 - Introduction to Computation(nonhons)
+%   {infoneapthree}  - Informatics 1 - Introduction to Computation(nonhons)
+%   {infonecg} - Informatics 1 - Cognitive Science          (nonhons)
+%   {infonecl} - Informatics 1 - Computation and Logic      (nonhons)
+%   {infoneda} - Informatics 1 - Data and Analysis          (nonhons)
+%   {infonefp} - Informatics 1 - Functional Programming     (nonhons)
+%   If there are two sittings of FP, use infonefpam for the first
+%   paper and infonefppm for the second sitting.
+%   {infoneop} - Informatics 1 - Object-Oriented Programming(nonhons)
+%   If there are two sittings of OOP, use infoneopam for the first
+%   paper and infoneoppm for the second sitting.
+%   {inftwoa}  - Informatics 2A: Proc. F&N Languages        (nonhons)
+%   {inftwob}  - Informatics 2B: Algs., D.Structs., Learning(nonhons)
+%   {inftwoccs}- Informatics 2C-CS: Computer Systems        (nonhons)
+%   {inftwocse}- Informatics 2C: Software Engineering       (nonhons)
+%   {inftwod}  - Informatics 2D: Reasoning and Agents       (nonhons)
+%   {iar}      - Intelligent Autonomous Robotics               (Inf4)
+%   {it}       - Information Theory                             (MSc)
+%   {imc}      - Introduction to Modern Cryptography           (Inf4)
+%   {iotssc}   - Internet of Things, Systems, Security and the Cloud   (Inf4)
+%   (iqc)      - Introduction to Quantum Computing             (Inf4)
+%   (itcs)     - Introduction to Theoretical Computer Science  (Inf3)
+%   {ivc}      - Image and Vision Computing			           (MSc)
+%   {ivr}      - Introduction to Vision and Robotics           (Inf3)
+%   {ivr-dl}   - Introduction to Vision and Robotics - distance learning (Msc)
+%   {iaml}     - Introductory Applied Machine Learning         (MSc)
+%   {iaml-dl}  - Introductory Applied Machine Learning - distance learning (MSc)
+%   {lpt}      - Logic Programming - Theory                    (Inf3)
+%   {lpp}      - Logic Programming - Programming               (Inf3)
+%   {mlpr}     - Machine Learning & Pattern Recognition        (Inf4)
+%   {mt}       - Machine Translation                           (Inf4)
+%   {mi}       - Music Informatics                              (MSc)
+%   {nlu}      - Natural Language Understanding [L11]          (Inf4)
+%   {nc}       - Neural Computation                             (MSc)
+%   {nat}      - Natural Computing                              (MSc)
+%   {nluplus}  - Natural Language Understanding, Generation, and Machine Translation(MSc)
+%   {nip}      - Neural Information Processing                  (MSc)
+%   {os}       - Operating Systems                             (Inf3)
+%   {pa}       - Parallel Architectures [L11]                  (Inf4)
+%   {pdiot}    - Principles and Design of IoT Systems          (Inf4)
+%   {ppls}     - Parallel Prog. Langs. and Sys. [L11]          (Inf4)
+%   {pm}       - Performance Modelling                         (Inf4)
+%   {pmr}      - Probabilistic Modelling and Reasoning          (MSc)
+%   {pi}       - Professional Issues                           (Inf3)
+%   {rc}       - Randomness and Computation                    (Inf4)
+%   {rl}       - Reinforcement Learning                         (MSc)
+%   {rlsc}     - Robot Learning and Sensorimotor Control        (MSc)
+%   {rss}      - Robotics: Science and Systems                  (MSc)
+%   {sp}       - Secure Programming                            (Inf4)
+%   {sws}      - Semantic Web Systems                          (Inf4)
+%   {stn}      - Social and Technological Networks             (Inf4)
+%   {sapm}     - Software Arch., Proc. and Mgmt. [L11]         (Inf4)
+%   {sdm}      - Software Design and Modelling                 (Inf3)
+%   {st}       - Software Testing                              (Inf3)
+%   {ttds}     - Text Technologies for Data Science            (Inf4)
+%   {tspl}     - Types and Semantics for Programming Langs.    (Inf4)
+%   {usec}     - Usable Security and Privacy                   (Inf4)
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\setcourse{tspl}
+\initcoursedata
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Set your exam rubric type.
+%
+% Most courses in the School have exams that add up to 50 marks,
+% and your choices are:
+%    {qu1_and_either_qu2_or_qu3, any_two_of_three, do_exam}
+% (which include the "CALCULATORS MAY NOT BE USED..." text), or
+%    {qu1_and_either_qu2_or_qu3_calc, any_two_of_three_calc, do_exam_calc}
+% (which DO NOT include the "CALCULATORS MAY NOT BE USED..." text), or
+%    {custom}.
+%
+% Note, if you opt to create a custom rubric, you must:
+%
+%   (i) **have permission** from the appropriate authority, and
+%  (ii) execute:
+%
+%        \setrubrictype{} to specify the custom rubric information.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\setrubric{qu1_and_either_qu2_or_qu3}
+
+\examtitlepage
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Manual override for total page number computation.
+%
+% As long as you run latex upon this document three times in a row,
+%  the right number of `total pages' should be computed and placed
+%  in the footer of all pages except the title page.
+%
+% But, if this fails, you can set that number yourself with the
+%  following command:
+%
+%    \settotalpages{n} with n a natural number.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Beginning of your exam text.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{enumerate}
+
+\item \rubricqA
+
+\newcommand{\Tree}{\texttt{Tree}}
+\newcommand{\AllT}{\texttt{AllT}}
+\newcommand{\AnyT}{\texttt{AnyT}}
+\newcommand{\leaf}{\texttt{leaf}}
+\newcommand{\branch}{\texttt{branch}}
+\newcommand{\here}{\texttt{here}}
+\renewcommand{\left}{\texttt{left}}
+\renewcommand{\right}{\texttt{right}}
+\newcommand{\ubar}{\texttt{\underline{~}}}
+
+Consider a type of trees defined as follows.
+\begin{gather*}
+%
+  \inference[\leaf]
+    {A}
+    {Tree~A}
+%
+\quad
+%
+  \inference[\ubar\branch\ubar]
+    {Tree~A \\
+     Tree~A}
+   {Tree~A}
+%
+\end{gather*}
+
+Given a predicate $P$ over $A$, we define predicates $\AllT$ and
+$\AnyT$ which hold when $P$ holds for \emph{every} leaf in the tree
+and when $P$ holds for \emph{some} leaf in the tree, respectively.
+\begin{gather*}
+%
+  \inference[\leaf]
+    {P~x}
+    {\AllT~P~(\leaf~x)}
+%
+\quad
+%
+  \inference[\ubar\branch\ubar]
+    {\AllT~P~xt \\
+     \AllT~P~yt}
+    {\AllT~P~(xt~\branch~yt)}
+%
+\\~\\
+%
+  \inference[\leaf]
+    {P~x}
+    {\AnyT~P~(\leaf~x)}
+%
+\quad
+%
+  \inference[\left]
+    {\AnyT~P~xt}
+    {\AnyT~P~(xt~\branch~yt)}
+%
+\quad
+%
+  \inference[\right]
+    {\AnyT~P~yt}
+    {\AnyT~P~(xt~\branch~yt)}
+%
+\end{gather*}
+
+\begin{itemize}
+
+\item[(a)] Formalise the definitions above.
+
+\marks{12}
+
+\item[(b)] Prove $\AllT~({\neg\ubar}~\circ~P)~xt$
+  implies $\neg~(\AnyT~P~xt)$, for all trees $xt$.
+
+\marks{13}
+
+\end{itemize}
+
+\newpage
+
+\item \rubricqB
+
+\newcommand{\COMP}{\texttt{Comp}}
+\newcommand{\OK}{\texttt{ok}}
+\newcommand{\ERROR}{\texttt{error}}
+\newcommand{\LETC}{\texttt{letc}}
+\newcommand{\IN}{\texttt{in}}
+
+\newcommand{\Comp}[1]{\COMP~#1}
+\newcommand{\error}[1]{\ERROR~#1}
+\newcommand{\ok}[1]{\OK~#1}
+\newcommand{\letc}[3]{\LETC~#1\leftarrow#2~\IN~#3}
+
+\newcommand{\comma}{\,,\,}
+\newcommand{\V}{\texttt{V}}
+\newcommand{\dash}{\texttt{-}}
+\newcommand{\Value}{\texttt{Value}}
+\newcommand{\becomes}{\longrightarrow}
+\newcommand{\subst}[3]{#1~\texttt{[}~#2~\texttt{:=}~#3~\texttt{]}}
+
+You will be provided with a definition of intrinsically-typed lambda
+calculus in Agda. Consider constructs satisfying the following rules,
+written in extrinsically-typed style.
+
+A computation of type $\Comp{A}$ returns either an error with a
+message $msg$ which is a string, or an ok value of a term $M$ of type $A$.
+Consider constructs satisfying the following rules:
+
+Typing:
+\begin{gather*}
+\inference[$\ERROR$]
+  {}
+  {\Gamma \vdash \error{msg} \typecolon \Comp{A}}
+\qquad
+\inference[$\OK$]
+  {\Gamma \vdash M \typecolon A}
+  {\Gamma \vdash \ok{M} \typecolon \Comp{A}}
+\\~\\
+\inference[$\LETC$]
+  {\Gamma \vdash M \typecolon \Comp{A} \\
+   \Gamma \comma x \typecolon A \vdash N \typecolon \Comp{B}}
+  {\Gamma \vdash \letc{x}{M}{N} \typecolon \Comp{B}}
+\end{gather*}
+
+Values:
+\begin{gather*}
+\inference[\V\dash\ERROR]
+  {}
+  {\Value~(\error{msg})}
+\qquad
+\inference[\V\dash\OK]
+  {\Value~V}
+  {\Value~(\ok{V})}
+\end{gather*}
+
+Reduction:
+\begin{gather*}
+\inference[$\xi\dash\OK$]
+  {M \becomes M'}
+  {\ok{M} \becomes \ok{M'}}
+\qquad
+\inference[$\xi\dash\LETC$]
+  {M \becomes M'}
+  {\letc{x}{M}{N} \becomes \letc{x}{M'}{N}}
+\\~\\
+\inference[$\beta\dash\ERROR$]
+  {}
+  {\letc{x}{(\error{msg})}{t} \becomes \error{msg}}
+\\~\\
+\inference[$\beta\dash\OK$]
+  {\Value{V}}
+  {\letc{x}{(\ok{V})}{N} \becomes \subst{N}{x}{V}}
+\end{gather*}
+
+\begin{enumerate}
+\item[(a)] Extend the given definition to formalise the evaluation
+           and typing rules, including any other required definitions.
+      \marks{12}
+
+\item[(b)] Prove progress. You will be provided with a proof of progress for
+           the simply-typed lambda calculus that you may extend.
+      \marks{13}
+\end{enumerate}
+
+Please delimit any code you add as follows.
+\begin{verbatim}
+-- begin
+-- end
+\end{verbatim}
+
+\newpage
+
+\item \rubricqC
+
+\newcommand{\TT}{\texttt{tt}}
+\newcommand{\CASETOP}{{\texttt{case}\top}}
+\newcommand{\casetop}[2]{\CASETOP~#1~{\texttt{[tt}\!\Rightarrow}~#2~\texttt{]}}
+\newcommand{\up}{\uparrow}
+\newcommand{\dn}{\downarrow}
+
+You will be provided with a definition of inference for extrinsically-typed lambda
+calculus in Agda. Consider constructs satisfying the following rules,
+written in extrinsically-typed style that support bidirectional inference.
+
+Typing:
+\begin{gather*}
+\inference[$\TT$]
+  {}
+  {\Gamma \vdash \TT \dn \top}
+\\~\\
+\inference[$\CASETOP$]
+  {\Gamma \vdash L \up \top \\
+   \Gamma \vdash M \dn A}
+  {\Gamma \vdash \casetop{L}{M} \dn A}
+\end{gather*}
+
+\begin{enumerate}
+\item[(a)] Extend the given definition to formalise the typing rules,
+      and update the definition of equality on types.
+      \marks{10}
+
+\item[(b)] Extend the code to support type inference for the new features.
+      \marks{15}
+\end{enumerate}
+
+Please delimit any code you add as follows.
+\begin{verbatim}
+-- begin
+-- end
+\end{verbatim}
+
+\end{enumerate}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% End of your exam text.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\end{document}
diff --git a/courses/tspl/2018/Mock2.tex b/courses/tspl/2018/Mock2.tex
new file mode 100644
index 00000000..33eb1306
--- /dev/null
+++ b/courses/tspl/2018/Mock2.tex
@@ -0,0 +1,407 @@
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% I N F O R M A T I C S
+%  Honours Exam LaTeX Template for Exam Authors
+%
+%  Created: 12-Oct-2009 by G.O.Passmore.
+%  Last Updated: 10-Sep-2018 by I. Murray
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%% The following define the status of the exam papers in the order
+%%% required.  Simply remove the comment (i.e., the % symbol) just
+%%% before the appropriate one and comment the others out.
+
+%\newcommand\status{\internal}
+%\newcommand\status{\external}
+\newcommand\status{\final}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%% The following three lines are always required.  You may add
+%%% custom packages to the one already defined if necessary.
+
+\documentclass{examhons2018}
+\usepackage{amssymb}
+\usepackage{amsmath}
+\usepackage{semantic}
+\usepackage{stix}
+
+%%% Uncomment the \checkmarksfalse line if the macros that check the
+%%% mark totals cause problems. However, please do not make your
+%%% questions add up to a non-standard number of marks without
+%%% permission of the convenor.
+%\checkmarksfalse
+
+\begin{document}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Replace {ad} below with the ITO code for your course.  This will
+%  be used by the ITO LaTeX installation to install course-specific
+%  data into the exam versions it produces from this document.
+%
+% Your choices are (in course title order):
+%
+%   {anlp}     - Acc. Natural Language Processing	            (MSc)
+%   {aleone}   - Adaptive Learning Environments 1              (Inf4)
+%   {adbs}     - Advanced Databases                            (Inf4)
+%   {av}       - Advanced Vision                               (Inf4)
+%   {av-dl}    - Advanced Vision - distance learning            (MSc)
+%   {apl}      - Advances in Programming Languages             (Inf4)
+%   {abs}      - Agent Based Systems [L10]                     (Inf3)
+%   {afds}     - Algorithmic Foundations of Data Science        (MSc)
+%   {agta}     - Algorithmic Game Theory and its Apps.          (MSc)
+%   {ads}      - Algorithms and Data Structures                (Inf3)
+%   {ad}       - Applied Databases                              (MSc)
+%   {aipf}     - Artificial Intelligence Present and Future     (MSc)
+%   {ar}       - Automated Reasoning 	                       (Inf3)
+%   {asr}      - Automatic Speech Recognition                  (Inf4)
+%   {bioone}   - Bioinformatics 1                               (MSc)
+%   {biotwo}   - Bioinformatics 2                               (MSc)
+%	{bdl}      - Blockchains and Distributed Ledgers		   (Inf4)
+%   {cqi}      - Categories and Quantum Informatics             (MSc)
+%   {copt}     - Compiler Opimisation [L11]                    (Inf4)
+%   {ct}       - Compiling Techniques                          (Inf3)
+%   {ccs}      - Computational Cognitive Science               (Inf3)
+%   {cmc}      - Computational Complexity                      (Inf4)
+%   {ca}       - Computer Algebra                              (Inf4)
+%   {cav}      - Computer Animation and Visualisation          (Inf4)
+%   {car}      - Computer Architecture                         (Inf3)
+%   {comn}     - Computer Comms. and Networks                  (Inf3)
+%   {cd}       - Computer Design                               (Inf3)
+%   {cg}       - Computer Graphics [L11]                       (Inf4)
+%   {cn}       - Computer Networking [L11]                     (Inf4)
+%   {cp}       - Computer Prog. Skills and Concepts         (nonhons)
+%   {cs}       - Computer Security                             (Inf3)
+%   {dds}      - Data, Design and Society                   (nonhons)
+%   {dme}      - Data Mining and Exploration                   (Msc)
+%   {dbs}      - Database Systems                              (Inf3)
+%   {dmr}      - Decision Making in Robots and Autonomous Agents(MSc)
+%   {dmmr}     - Discrete Maths. and Math. Reasoning        (nonhons)
+%   {ds}       - Distributed Systems [L11]                     (Inf4)
+%   {epl}      - Elements of Programming Languages             (Inf3)
+%   {es}       - Embedded Software                             (Inf4)
+%   {exc}      - Extreme Computing                             (Inf4)
+%   {fv}       - Formal Verification                           (Inf4)
+%   {fnlp}     - Foundations of Natural Language Processing    (Inf3)
+%   {hci}      - Human-Computer Interaction [L11]              (Inf4)
+%   {infonea}  - Informatics 1 - Introduction to Computation(nonhons)
+%   different sittings for INF1A programming exams
+%   {infoneapone}  - Informatics 1 - Introduction to Computation(nonhons)
+%   {infoneaptwo}  - Informatics 1 - Introduction to Computation(nonhons)
+%   {infoneapthree}  - Informatics 1 - Introduction to Computation(nonhons)
+%   {infonecg} - Informatics 1 - Cognitive Science          (nonhons)
+%   {infonecl} - Informatics 1 - Computation and Logic      (nonhons)
+%   {infoneda} - Informatics 1 - Data and Analysis          (nonhons)
+%   {infonefp} - Informatics 1 - Functional Programming     (nonhons)
+%   If there are two sittings of FP, use infonefpam for the first
+%   paper and infonefppm for the second sitting.
+%   {infoneop} - Informatics 1 - Object-Oriented Programming(nonhons)
+%   If there are two sittings of OOP, use infoneopam for the first
+%   paper and infoneoppm for the second sitting.
+%   {inftwoa}  - Informatics 2A: Proc. F&N Languages        (nonhons)
+%   {inftwob}  - Informatics 2B: Algs., D.Structs., Learning(nonhons)
+%   {inftwoccs}- Informatics 2C-CS: Computer Systems        (nonhons)
+%   {inftwocse}- Informatics 2C: Software Engineering       (nonhons)
+%   {inftwod}  - Informatics 2D: Reasoning and Agents       (nonhons)
+%   {iar}      - Intelligent Autonomous Robotics               (Inf4)
+%   {it}       - Information Theory                             (MSc)
+%   {imc}      - Introduction to Modern Cryptography           (Inf4)
+%   {iotssc}   - Internet of Things, Systems, Security and the Cloud   (Inf4)
+%   (iqc)      - Introduction to Quantum Computing             (Inf4)
+%   (itcs)     - Introduction to Theoretical Computer Science  (Inf3)
+%   {ivc}      - Image and Vision Computing			           (MSc)
+%   {ivr}      - Introduction to Vision and Robotics           (Inf3)
+%   {ivr-dl}   - Introduction to Vision and Robotics - distance learning (Msc)
+%   {iaml}     - Introductory Applied Machine Learning         (MSc)
+%   {iaml-dl}  - Introductory Applied Machine Learning - distance learning (MSc)
+%   {lpt}      - Logic Programming - Theory                    (Inf3)
+%   {lpp}      - Logic Programming - Programming               (Inf3)
+%   {mlpr}     - Machine Learning & Pattern Recognition        (Inf4)
+%   {mt}       - Machine Translation                           (Inf4)
+%   {mi}       - Music Informatics                              (MSc)
+%   {nlu}      - Natural Language Understanding [L11]          (Inf4)
+%   {nc}       - Neural Computation                             (MSc)
+%   {nat}      - Natural Computing                              (MSc)
+%   {nluplus}  - Natural Language Understanding, Generation, and Machine Translation(MSc)
+%   {nip}      - Neural Information Processing                  (MSc)
+%   {os}       - Operating Systems                             (Inf3)
+%   {pa}       - Parallel Architectures [L11]                  (Inf4)
+%   {pdiot}    - Principles and Design of IoT Systems          (Inf4)
+%   {ppls}     - Parallel Prog. Langs. and Sys. [L11]          (Inf4)
+%   {pm}       - Performance Modelling                         (Inf4)
+%   {pmr}      - Probabilistic Modelling and Reasoning          (MSc)
+%   {pi}       - Professional Issues                           (Inf3)
+%   {rc}       - Randomness and Computation                    (Inf4)
+%   {rl}       - Reinforcement Learning                         (MSc)
+%   {rlsc}     - Robot Learning and Sensorimotor Control        (MSc)
+%   {rss}      - Robotics: Science and Systems                  (MSc)
+%   {sp}       - Secure Programming                            (Inf4)
+%   {sws}      - Semantic Web Systems                          (Inf4)
+%   {stn}      - Social and Technological Networks             (Inf4)
+%   {sapm}     - Software Arch., Proc. and Mgmt. [L11]         (Inf4)
+%   {sdm}      - Software Design and Modelling                 (Inf3)
+%   {st}       - Software Testing                              (Inf3)
+%   {ttds}     - Text Technologies for Data Science            (Inf4)
+%   {tspl}     - Types and Semantics for Programming Langs.    (Inf4)
+%   {usec}     - Usable Security and Privacy                   (Inf4)
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\setcourse{tspl}
+\initcoursedata
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Set your exam rubric type.
+%
+% Most courses in the School have exams that add up to 50 marks,
+% and your choices are:
+%    {qu1_and_either_qu2_or_qu3, any_two_of_three, do_exam}
+% (which include the "CALCULATORS MAY NOT BE USED..." text), or
+%    {qu1_and_either_qu2_or_qu3_calc, any_two_of_three_calc, do_exam_calc}
+% (which DO NOT include the "CALCULATORS MAY NOT BE USED..." text), or
+%    {custom}.
+%
+% Note, if you opt to create a custom rubric, you must:
+%
+%   (i) **have permission** from the appropriate authority, and
+%  (ii) execute:
+%
+%        \setrubrictype{} to specify the custom rubric information.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\setrubric{qu1_and_either_qu2_or_qu3}
+
+\examtitlepage
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Manual override for total page number computation.
+%
+% As long as you run latex upon this document three times in a row,
+%  the right number of `total pages' should be computed and placed
+%  in the footer of all pages except the title page.
+%
+% But, if this fails, you can set that number yourself with the
+%  following command:
+%
+%    \settotalpages{n} with n a natural number.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Beginning of your exam text.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{enumerate}
+
+\item \rubricqA
+
+\newcommand{\key}{\texttt}
+\newcommand{\List}{\key{list}}
+\newcommand{\nil}{\texttt{[]}}
+\newcommand{\cons}{\mathbin{\key{::}}}
+\newcommand{\member}{\key{member}}
+\newcommand{\sublist}{\key{sublist}}
+
+This question uses the library definition of $\List$ in Agda.
+Here is an informal definition of the predicates $\in$
+and $\subseteq$.  (In Emacs, you can type $\in$ as \verb$\in$ and $\subseteq$ as \verb$\subseteq$.)
+$\subseteq$
+\begin{gather*}
+\inference[$\key{here}$]
+  {}
+  {x \in (x \cons xs)}
+\qquad
+\inference[$\key{there}$]
+  {x \in ys}
+  {x \in (y \cons ys)}
+\\~\\
+\inference[$\key{done}$]
+  {}
+  {\nil \subseteq ys}
+\\~\\
+\inference[$\key{keep}$]
+  {xs \subseteq ys}
+  {(x \cons xs) \subseteq (x \cons ys)}
+\qquad
+\inference[$\key{drop}$]
+  {xs \subseteq ys}
+  {xs \subseteq (y \cons ys)}
+\end{gather*}
+
+\begin{itemize}
+
+\item[(a)] Formalise the definition above.
+\marks{10}
+
+\item[(b)] Prove each of the following.
+  \begin{itemize}
+  \item[(i)]  $\key{2} \in \key{[1,2,3]}$
+  \item[(ii)]  $\key{[1,3]} \subseteq \key{[1,2,3,4]}$
+  \end{itemize}
+\marks{5}
+
+\item[(c)] Prove the following.
+\begin{center}
+If $xs \subseteq ys$ then $z \in xs$ implies $z \in ys$ for all $z$.
+\end{center}
+\marks{10}
+
+\end{itemize}
+
+\newpage
+
+\item \rubricqB
+
+\newcommand{\Tree}{\texttt{Tree}}
+\newcommand{\leaf}{\texttt{leaf}}
+\newcommand{\branch}{\texttt{branch}}
+\newcommand{\CASET}{\texttt{caseT}}
+\newcommand{\caseT}[6]{\texttt{case}~#1~\texttt{[leaf}~#2~\Rightarrow~#3~\texttt{|}~#4~\texttt{branch}~#5~\Rightarrow~#6\texttt{]}}
+\newcommand{\ubar}{\texttt{\underline{~}}}
+\newcommand{\comma}{\,\texttt{,}\,}
+\newcommand{\V}{\texttt{V}}
+\newcommand{\dash}{\texttt{-}}
+\newcommand{\Value}{\texttt{Value}}
+\newcommand{\becomes}{\longrightarrow}
+\newcommand{\subst}[3]{#1~\texttt{[}~#2~\texttt{:=}~#3~\texttt{]}}
+
+
+You will be provided with a definition of intrinsically-typed lambda
+calculus in Agda. Consider constructs satisfying the following rules,
+written in extrinsically-typed style.
+
+Typing:
+\begin{gather*}
+  \inference[\leaf]
+    {\Gamma \vdash M \typecolon A}
+    {\Gamma \vdash \leaf~M \typecolon \Tree~A}
+\quad
+  \inference[\branch]
+    {\Gamma \vdash M \typecolon \Tree~A \\
+     \Gamma \vdash N \typecolon \Tree~A}
+    {\Gamma \vdash M~\branch~N \typecolon \Tree~A}
+\\~\\
+  \inference[\CASET]
+    {\Gamma \vdash L \typecolon \Tree~A \\
+     \Gamma \comma x \typecolon A \vdash M \typecolon B \\
+     \Gamma \comma y \typecolon \Tree~A \comma z \typecolon \Tree~A \vdash N \typecolon B}
+    {\Gamma \vdash \caseT{L}{x}{M}{y}{z}{N} \typecolon B}
+\end{gather*}
+
+Values:
+\begin{gather*}
+\inference[\V\dash\leaf]
+  {\Value~V}
+  {\Value~(\leaf~V)}
+\qquad
+\inference[\V\dash\branch]
+  {\Value~V \\
+   \Value~W}
+  {\Value~(V~\branch~W)}
+\end{gather*}
+
+Reduction:
+\begin{gather*}
+\inference[$\xi\dash\leaf$]
+  {M \becomes M'}
+  {\leaf{M} \becomes \leaf{M'}}
+\\~\\
+\inference[$\xi\dash\branch_1$]
+  {M \becomes M'}
+  {M~\branch~N \becomes M'~\branch~N}
+\qquad
+\inference[$\xi\dash\branch_2$]
+  {\Value~V \\
+   N \becomes N'}
+  {V~\branch~N \becomes V~\branch~N'}
+\\~\\
+\inference[$\xi\dash\CASET$]
+  {L \becomes L'}
+  {\begin{array}{c}
+     \caseT{L}{x}{M}{y}{z}{N} \becomes \\
+     {} \quad \caseT{L'}{x}{M}{y}{z}{N}
+   \end{array}}
+\\~\\
+\inference[$\beta\dash\leaf$]
+  {\Value~V}
+  {\caseT{(\leaf~V)}{x}{M}{y}{z}{N} \becomes \subst{M}{x}{V}}
+\\~\\
+\inference[$\beta\dash\branch$]
+  {\Value~V \\
+   \Value~W}
+  {\caseT{(V~\branch~W)}{x}{M}{y}{z}{N} \becomes \subst{\subst{N}{y}{V}}{z}{W}}
+\end{gather*}
+
+\begin{enumerate}
+\item[(a)] Extend the given definition to formalise the evaluation and
+  typing rules, including any other required definitions.
+      \marks{12}
+
+\item[(b)] Prove progress. You will be provided with a proof of
+  progress for the simply-typed lambda calculus that you may
+  extend.
+      \marks{13}
+\end{enumerate}
+
+Please delimit any code you add as follows.
+\begin{verbatim}
+-- begin
+-- end
+\end{verbatim}
+
+\newpage
+
+\item \rubricqC
+
+\newcommand{\Lift}{\texttt{Lift}}
+\newcommand{\delay}{\texttt{delay}}
+\newcommand{\force}{\texttt{force}}
+\newcommand{\up}{\uparrow}
+\newcommand{\dn}{\downarrow}
+
+You will be provided with a definition of inference for extrinsically-typed lambda
+calculus in Agda. Consider constructs satisfying the following rules,
+written in extrinsically-typed style that support bidirectional inference.
+
+Typing:
+\begin{gather*}
+\inference[$\delay$]
+  {\Gamma \vdash M \dn A}
+  {\Gamma \vdash \delay~M \dn \Lift~A}
+\\~\\
+\inference[$\force$]
+  {\Gamma \vdash L \up \Lift~A}
+  {\Gamma \vdash \force~L \up A}
+\end{gather*}
+
+\begin{enumerate}
+\item[(a)] Extend the given definition to formalise the typing rules,
+and update the definition of equality on types.
+      \marks{10}
+
+\item[(b)] Extend the code to support type inference for the new features.
+      \marks{15}
+\end{enumerate}
+
+Please delimit any code you add as follows.
+\begin{verbatim}
+-- begin
+-- end
+\end{verbatim}
+
+\end{enumerate}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% End of your exam text.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\end{document}
diff --git a/courses/tspl/2018/examhons2018.cls b/courses/tspl/2018/examhons2018.cls
new file mode 100644
index 00000000..73e31e10
--- /dev/null
+++ b/courses/tspl/2018/examhons2018.cls
@@ -0,0 +1,1246 @@
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% I N F O R M A T I C S
+%  Honours Exam LaTeX Package v0.1
+%
+%  Created: 12-Oct-2009 by G.O.Passmore.
+%  Last Updated: 11-07-2017 by G.Hall
+%
+%  Note: We are changing the file and package name of this style
+%   from year to year, so as to make people aware of the version
+%   they are using.  The format is `examhons<YYYY>.sty' with <YYYY>
+%   replaced appropriately.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\NeedsTeXFormat{LaTeX2e}[1995/12/01]
+\ProvidesClass{examhons2016}[2009/10/12 v0.1 (GOP)]
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Set the ITO path for status.tex.
+%
+% * Note that course organisers / exam preparers do not need
+%    status.tex.  When building their exam on their own machines,
+%    the exam title / date / etc. information will be automatically
+%    filled-in with dummy values for mock-up purposes.
+%
+%    Once the exam document is processed on the ITO machines,
+%    however, the mock-up exam title / date / etc. data will be
+%    overwritten with the officially sanctioned data held in
+%    the ITO's master status.tex file.
+%
+%  This file resides in the relative path below.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\def\itostatuspath{../exam-macros/}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Inherit the proper letter class.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\LoadClass[12pt,a4paper]{article}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Take care of `page x of y' the proper way, based on a combination
+%  of the J. Goldberg (lastpage) method, the C. Huggins (using fh)
+%  code, woven together with some use of the ifthen package for
+%  branching on p0 (the exam title page, which shouldn't be num'd).
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\RequirePackage{fancyhdr,ifthen,a4}
+\pagestyle{fancy}
+\fancyhf{}
+
+\def\lastpage@putlabel{\addtocounter{page}{-1}%
+   \immediate\write\@auxout{\string
+   \newlabel{LastPage}{{}{\thepage}}}%
+   \addtocounter{page}{1}}
+
+\AtEndDocument{%
+   \message{*** Setting LastPage: Make sure you
+     run LaTeX upon your exam file at least 3
+     times to get this right.}%
+   \clearpage\lastpage@putlabel}%
+
+\newcommand{\totalpagesoverride}{0}
+
+ {\rfoot{\ifthenelse{\totalpagesoverride=0}
+          {\ifthenelse{\thepage>0}
+           {\scriptsize{Page \thepage{} of \pageref{LastPage}}}
+           {}}
+          {{\scriptsize{Page \thepage{} of \@forcedtotalpages}}}}}
+
+
+\renewcommand\headrulewidth{0pt}
+
+\newcommand{\settotalpages}[1]{
+ \def\@forcedtotalpages{#1}
+ \renewcommand{\totalpagesoverride}{1}}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Inlining of the EPSF package by Rokicki et al.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\newread\epsffilein    % file to \read
+\newif\ifepsffileok    % continue looking for the bounding box?
+\newif\ifepsfbbfound   % success?
+\newif\ifepsfverbose   % report what you're making?
+\newif\ifepsfdraft     % use draft mode?
+\newdimen\epsfxsize    % horizontal size after scaling
+\newdimen\epsfysize    % vertical size after scaling
+\newdimen\epsftsize    % horizontal size before scaling
+\newdimen\epsfrsize    % vertical size before scaling
+\newdimen\epsftmp      % register for arithmetic manipulation
+\newdimen\pspoints     % conversion factor
+%
+\pspoints=1bp          % Adobe points are `big'
+\epsfxsize=0pt         % Default value, means `use natural size'
+\epsfysize=0pt         % ditto
+%
+\def\epsfbox#1{\global\def\epsfllx{72}\global\def\epsflly{72}%
+   \global\def\epsfurx{540}\global\def\epsfury{720}%
+   \def\lbracket{[}\def\testit{#1}\ifx\testit\lbracket
+   \let\next=\epsfgetlitbb\else\let\next=\epsfnormal\fi\next{#1}}%
+%
+\def\epsfgetlitbb#1#2 #3 #4 #5]#6{\epsfgrab #2 #3 #4 #5 .\\%
+   \epsfsetgraph{#6}}%
+%
+\def\epsfnormal#1{\epsfgetbb{#1}\epsfsetgraph{#1}}%
+%
+\def\epsfgetbb#1{%
+%
+%   The first thing we need to do is to open the
+%   PostScript file, if possible.
+%
+\openin\epsffilein=#1
+\ifeof\epsffilein\errmessage{I couldn't open #1, will ignore it}\else
+%
+%   Okay, we got it. Now we'll scan lines until we find one that doesn't
+%   start with %. We're looking for the bounding box comment.
+%
+   {\epsffileoktrue \chardef\other=12
+    \def\do##1{\catcode`##1=\other}\dospecials \catcode`\ =10
+    \loop
+       \read\epsffilein to \epsffileline
+       \ifeof\epsffilein\epsffileokfalse\else
+%
+%   We check to see if the first character is a % sign;
+%   if not, we stop reading (unless the line was entirely blank);
+%   if so, we look further and stop only if the line begins with
+%   `%%BoundingBox:'.
+%
+          \expandafter\epsfaux\epsffileline:. \\%
+       \fi
+   \ifepsffileok\repeat
+   \ifepsfbbfound\else
+    \ifepsfverbose\message{No bounding box comment in #1; using defaults}\fi\fi
+   }\closein\epsffilein\fi}%
+%
+%   Now we have to calculate the scale and offset values to use.
+%   First we compute the natural sizes.
+%
+\def\epsfclipon{\def\epsfclipstring{ clip}}%
+\def\epsfclipoff{\def\epsfclipstring{\ifepsfdraft\space clip\fi}}%
+\epsfclipoff
+%
+\def\epsfsetgraph#1{%
+   \epsfrsize=\epsfury\pspoints
+   \advance\epsfrsize by-\epsflly\pspoints
+   \epsftsize=\epsfurx\pspoints
+   \advance\epsftsize by-\epsfllx\pspoints
+%
+%   If `epsfxsize' is 0, we default to the natural size of the picture.
+%   Otherwise we scale the graph to be \epsfxsize wide.
+%
+   \epsfxsize\epsfsize\epsftsize\epsfrsize
+   \ifnum\epsfxsize=0 \ifnum\epsfysize=0
+      \epsfxsize=\epsftsize \epsfysize=\epsfrsize
+      \epsfrsize=0pt
+%
+%   We have a sticky problem here:  TeX doesn't do floating point arithmetic!
+%   Our goal is to compute y = rx/t. The following loop does this reasonably
+%   fast, with an error of at most about 16 sp (about 1/4000 pt).
+%
+     \else\epsftmp=\epsftsize \divide\epsftmp\epsfrsize
+       \epsfxsize=\epsfysize \multiply\epsfxsize\epsftmp
+       \multiply\epsftmp\epsfrsize \advance\epsftsize-\epsftmp
+       \epsftmp=\epsfysize
+       \loop \advance\epsftsize\epsftsize \divide\epsftmp 2
+       \ifnum\epsftmp>0
+          \ifnum\epsftsize<\epsfrsize\else
+             \advance\epsftsize-\epsfrsize \advance\epsfxsize\epsftmp \fi
+       \repeat
+       \epsfrsize=0pt
+     \fi
+   \else \ifnum\epsfysize=0
+     \epsftmp=\epsfrsize \divide\epsftmp\epsftsize
+     \epsfysize=\epsfxsize \multiply\epsfysize\epsftmp
+     \multiply\epsftmp\epsftsize \advance\epsfrsize-\epsftmp
+     \epsftmp=\epsfxsize
+     \loop \advance\epsfrsize\epsfrsize \divide\epsftmp 2
+     \ifnum\epsftmp>0
+        \ifnum\epsfrsize<\epsftsize\else
+           \advance\epsfrsize-\epsftsize \advance\epsfysize\epsftmp \fi
+     \repeat
+     \epsfrsize=0pt
+    \else
+     \epsfrsize=\epsfysize
+    \fi
+   \fi
+%
+%  Finally, we make the vbox and stick in a \special that dvips can parse.
+%
+   \ifepsfverbose\message{#1: width=\the\epsfxsize, height=\the\epsfysize}\fi
+   \epsftmp=10\epsfxsize \divide\epsftmp\pspoints
+   \vbox to\epsfysize{\vfil\hbox to\epsfxsize{%
+      \ifnum\epsfrsize=0\relax
+        \special{PSfile=\ifepsfdraft psdraft.ps\else#1\fi\space
+             llx=\epsfllx\space lly=\epsflly\space
+             urx=\epsfurx\space ury=\epsfury\space rwi=\number\epsftmp
+             \epsfclipstring}%
+      \else
+        \epsfrsize=10\epsfysize \divide\epsfrsize\pspoints
+        \special{PSfile=\ifepsfdraft psdraft.ps\else#1\fi\space
+             llx=\epsfllx\space lly=\epsflly\space
+             urx=\epsfurx\space ury=\epsfury\space rwi=\number\epsftmp\space
+             rhi=\number\epsfrsize \epsfclipstring}%
+      \fi
+      \hfil}}%
+\global\epsfxsize=0pt\global\epsfysize=0pt}%
+%
+%   We still need to define the tricky \epsfaux macro. This requires
+%   a couple of magic constants for comparison purposes.
+%
+{\catcode`\%=12 \global\let\epsfpercent=%\global\def\epsfbblit{%BoundingBox}}%
+%
+%   So we're ready to check for `%BoundingBox:' and to grab the
+%   values if they are found.
+%
+\long\def\epsfaux#1#2:#3\\{\ifx#1\epsfpercent
+   \def\testit{#2}\ifx\testit\epsfbblit
+      \epsfgrab #3 . . . \\%
+      \epsffileokfalse
+      \global\epsfbbfoundtrue
+   \fi\else\ifx#1\par\else\epsffileokfalse\fi\fi}%
+%
+%   Here we grab the values and stuff them in the appropriate definitions.
+%
+\def\epsfempty{}%
+\def\epsfgrab #1 #2 #3 #4 #5\\{%
+\global\def\epsfllx{#1}\ifx\epsfllx\epsfempty
+      \epsfgrab #2 #3 #4 #5 .\\\else
+   \global\def\epsflly{#2}%
+   \global\def\epsfurx{#3}\global\def\epsfury{#4}\fi}%
+%
+%   We default the epsfsize macro.
+%
+\def\epsfsize#1#2{\epsfxsize}
+%
+%   Finally, another definition for compatibility with older macros.
+%
+\let\epsffile=\epsfbox
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Inlining of the UK date package by A. Clark.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\def\@cent{\count0 }
+\def\@diy{\count1 }
+\def\@dow{\count2 }
+\def\@epact{\count3 }
+\def\@golden{\count4 }
+\def\@leap{\count5 }
+\def\@x{\count6 }
+\def\@y{\count7 }
+
+\def\@up#1{{\@savestyle\thinspace$^{\underline{\hbox{%
+  \scriptsize\@setstyle#1\fam=-1 }}}$}}
+\def\st{\@up{st}}
+\def\nd{\@up{nd}}
+\def\rd{\@up{rd}}
+\def\th{\@up{th}}
+
+\def\@savestyle{\count0=\the\fam}
+\def\@setstyle{\ifcase\count0\rm\or\mit\or\cal\or\rm
+  \or\it\or\sl\or\bf\or\tt\fi}
+
+\def\today{\dayofweek{} \number\day\ifcase\day
+  \or\st\or\nd\or\rd\or\th\or\th\or\th\or\th\or\th\or\th\or\th
+  \or\th\or\th\or\th\or\th\or\th\or\th\or\th\or\th\or\th\or\th
+  \or\st\or\nd\or\rd\or\th\or\th\or\th\or\th\or\th\or\th\or\th\or\st\fi
+  \space\ifcase\month\or January\or February\or March\or April\or May\or
+  June\or July\or August\or September\or October\or November\or December\fi
+  \space\number\year}
+
+\def\dayofweek{{%
+  \@leap=\month \advance\@leap by -14 \divide\@leap by 12
+  \advance\@leap by \year
+  \@dow=\month \advance\@dow by 10
+  \@y=\@dow \divide\@y by 13 \multiply\@y by 12
+  \advance\@dow by -\@y \multiply\@dow by 13
+  \advance\@dow by -1 \divide\@dow by 5
+  \advance\@dow by \day \advance\@dow by 77
+  \@x=\@leap \@y=\@x \divide\@y by 100 \multiply\@y by 100 \advance\@x by -\@y
+  \multiply\@x by 5 \divide\@x by 4 \advance\@dow by \@x
+  \@x=\@leap \divide\@x by 400 \advance\@dow by \@x
+  \@x=\@leap \divide\@x by 100 \multiply\@x by 2 \advance\@dow by -\@x
+  \@x=\@dow \divide\@x by 7 \multiply\@x by 7 \advance\@dow by -\@x
+  \ifcase\@dow Sunday\or Monday\or Tuesday\or Wednesday\or
+      Thursday\or Friday\or Saturday\fi}}
+\def\phaseofmoon{{%
+  \@diy=\day \advance\@diy by \ifcase\month
+      -1\or -1\or 30\or 58\or 89\or 119\or 150\or
+      180\or 211\or 241\or 272\or 303\or 333\fi
+  \ifnum \month>2
+    \@x=\year \@y=\@x \divide\@y by 4 \multiply\@y by 4 \advance\@x by -\@y
+    \ifnum \@x=0
+      \@x=\year \@y=\@x \divide\@y by 400
+      \multiply\@y by 400 \advance\@x by -\@y
+      \ifnum \@x=0
+      \advance\@diy by 1
+      \else
+      \@x=\year \@y=\@x \divide\@y by 100
+      \multiply\@y by 100 \advance\@x by -\@y
+      \ifnum \@x>0
+          \advance\@diy by 1
+      \fi
+      \fi
+    \fi
+  \fi
+  \@cent=\year \divide\@cent by 100 \advance\@cent by 1
+  \@golden=\year
+  \@y=\year \divide\@y by 19 \multiply\@y by 19 \advance\@golden by -\@y
+  \advance\@golden by 1
+  \@epact=11 \multiply\@epact by \@golden
+  \advance\@epact by 20
+  \@x=8 \multiply\@x by \@cent \advance\@x by 5
+  \divide\@x by 25 \advance\@x by -5
+  \advance\@epact by \@x
+  \@x=3 \multiply\@x by \@cent \divide\@x by 4 \advance\@x by -12
+  \advance\@epact by -\@x
+  \@y=\@epact \divide\@y by 30 \multiply\@y by 30 \advance\@epact by -\@y
+  \ifnum \@epact<0
+    \advance\@epact by 30
+  \fi
+  \ifnum \@epact=25
+    \ifnum \@golden>11
+      \advance \@epact by 1
+    \fi
+  \else
+    \ifnum \@epact=24
+      \advance \@epact by 1
+    \fi
+  \fi
+  \@x=\@diy \advance\@x by \@epact \multiply\@x by 6 \advance\@x by 11
+  \@y=\@x \divide\@y by 177 \multiply\@y by 177 \advance\@x by -\@y
+  \divide\@x by 22
+  \ifcase\@x new\or waxing crescent\or in its first quarter\or
+      waxing gibbous\or full\or waning gibbous\or
+      in its last quarter\or waning crescent\or new\fi}}
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Now, we want to define commands for exam title, time, conveners,
+%  and so on, *but* we want to provide hard-coded dummy values
+%  for exam preparers who are working on their own machines.
+%  This is so that status.tex does not need to be ever copied from
+%  the ITO installation; it is only for ITO.
+%
+% The logic here is simple.  If we find \itostatuspath status.tex
+%  to exist, then we populate the values of exam title, time, and
+%  so on using those it contains corresponding to \courseid, which
+%  is set by the exam preparer using the \setcourse command.
+%  This is done internally by executing a command named
+%  \<courseid>details, with <courseid> replaced by their courseid.
+%
+% Otherwise, we use dummy values, but we've gone to the effort to
+%  at least include the correct course title and type (Inf3,MSc,..)
+%  within these mock values so as to keep the preparer happy ;-).
+%
+% Once that's done, we need to work out the rubric.  The rubric
+%  is printed on the title page and is set by the exam author
+%  using the \setrubric command.  They have the following options:
+%
+%   {qu1_and_either_qu2_or_qu3, any_two_of_three, custom}.
+%
+% Again, the usage of this information follows the same structure
+%  as above.  On an ITO machine, the master files are sourced from
+%  the itostatuspath directory.  On an exam preparer's machine,
+%  we generate mock-up values for the rubric form and type.
+%
+% Note, if they create a custom rubric, they must then execute:
+%
+%  \setrubricform{} and \setrubrictype to specify the custom
+%   rubric information.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\newcommand{\coursestatusfcn}{}
+\newcommand{\courseid}{}
+\newcommand{\rubricid}{}
+\newcommand{\rubricform}{}
+\newcommand{\rubrictype}{}
+
+\providecommand{\status}{}
+
+\newcommand{\setcourse}[1]{
+ \renewcommand{\courseid}{#1}
+}
+
+\newcommand{\setrubric}[1]{\renewcommand{\rubricid}{#1}}
+\newcommand{\setrubricform}[1]{\renewcommand{\rubricform}{#1}}
+\newcommand{\setrubrictype}[1]{\renewcommand{\rubrictype}{#1}}
+
+\AtBeginDocument{
+ \newcounter{Day}   \setcounter{Day}{\day}
+ \newcounter{Month} \setcounter{Month}{\month}
+ \newcounter{Year}  \setcounter{Year}{\year}
+}
+
+\newenvironment{hint}{\par[{\bf Hint:} }{\nolinebreak]}
+\newenvironment{hints}{\par[{\bf Hints:} }{\nolinebreak]}
+\newenvironment{note}{\par[{\bf Note:} }{\nolinebreak]}
+\newenvironment{notes}{\par[{\bf Notes:} }{\nolinebreak]}
+
+\def\ps@header{\let\@mkboth\@gobbletwo
+     \let\@oddfoot\@empty\let\@evenhead\@empty\let\@evenfoot\@oddfoot}
+\def\setstatus#1{\def\@status{#1}}
+\def\@status{}
+\def\@nextone{f}\def\@nextbutone{f}%
+\def\@oddhead{{\bf\it \@status}\hfil\it\@conthead}
+\def\@conthead{\if\@nextone t\relax QUESTION CONTINUED FROM PREVIOUS PAGE\fi\xdef\@nextone{\@nextbutone}\gdef\@nextbutone{f}}
+\def\continued{%
+\gdef\@nextbutone{t}
+\par\rightline{\it QUESTION CONTINUES ON NEXT PAGE}\newpage%
+}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Display the exam status (for `internal'/`external' scrutiny, or
+%  `final' which will print no corresponding notice).
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\def\internal{
+  \setstatus{\it FOR INTERNAL SCRUTINY (date of this version: \theDay/\theMonth/\theYear)}}
+\def\external{
+  \setstatus{\it FOR EXTERNAL EXAMINER (date of this version: \theDay/\theMonth/\theYear)}}
+\def\final{\setstatus{}}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Setup the proper marks displays.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\def\Marks#1#2{\marginpar{\raisebox{#2\baselineskip}{[{\it #1
+  \ifnum #1=1 mark\else marks\fi\/}]}}}
+%Version for most situations.
+\def\marks#1{\Marks{#1}{0}}
+% The next version is to get around the problem that you cannot put a
+% marginpar in maths display.  Put \marksl just before the display line.
+\def\marksd#1{\Marks{#1}{-2}}
+% As above but raises the box.
+\def\marksu#1{\Marks{#1}{1}}
+
+\leftmargini=0pt
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% EPS macros by KK.
+%
+% The first argument is the filename and the second the size (of the
+%  x-axis or the y-axis respectively.
+%
+% For example \psfigx{graph1.epsf}{5in} will input your first graph
+%  and make the x-axis equal to 4.5in, with the y-axis appropriately
+%  scaled.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\def\psfigx#1#2{
+  \begin{center}
+     \leavevmode
+     \epsfxsize=#2
+     \epsffile{#1}
+   \end{center}}
+
+\def\psfigy#1#2{
+  \begin{center}
+     \leavevmode
+     \epsfysize=#2
+     \epsffile{#1}
+   \end{center}}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Commands for manipulating exam course data.
+%
+% We will use them to assign dummy values on exam preparer machines,
+%  and otherwise will source the master ITO status.tex if it exists
+%  (e.g., when we are compiling on an ITO machine).
+%
+% Also, the papertype.inc files and rubric.inc files will be
+%  loaded if we are on an ITO machine.  Otherwise, we will provide
+%  dummy mock-up values for those as well.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\newcommand\papertitle[1]{\global\def\nameofpaper{\uppercase{#1}}}
+\newcommand\papertype[1]{\global\def\typeofpaper{
+ \InputIfFileExists{\itostatuspath #1}{}
+  {
+    %
+    % If we're here, then this is running on exam preparer's
+    % machine.  So, we will use mock-up values for the exam
+    % type text corresponding to #1.
+    %
+    % Options for #1 are {msc.inc, inf4msc.inc, inf3.inc, inf4.inc,
+    %                     nonhons.inc}.
+    %
+
+   \ifthenelse{\equal{#1}{msc.inc}}
+     {MSc Courses
+       \vskip 0.1in
+      Convener: ITO-Will-Determine\\
+      External Examiners: ITO-Will-Determine}{}
+   \ifthenelse{\equal{#1}{inf4msc.inc}}
+     {Year 4 Courses
+       \vskip 0.1in
+      Convener: ITO-Will-Determine\\
+      External Examiners: ITO-Will-Determine
+       \vskip 0.5in
+      MSc Courses
+       \vskip 0.1in
+      Convener: ITO-Will-Determine\\
+      External Examiners: ITO-Will-Determine}{}
+   \ifthenelse{\equal{#1}{inf3inf4.inc}}
+     {Year 3 Courses
+       \vskip 0.1in
+      Convenor: ITO-Will-Determine\\
+      External Examiners: ITO-Will-Determine
+       \vskip 0.5in
+      Year 4 Courses
+       \vskip 0.1in
+      Convener: ITO-Will-Determine\\
+      External Examiners: ITO-Will-Determine}{}
+   \ifthenelse{\equal{#1}{inf3.inc}}
+     {Year 3 Courses
+       \vskip 0.1in
+      Convener: ITO-Will-Determine\\
+      External Examiners: ITO-Will-Determine}{}
+   \ifthenelse{\equal{#1}{inf4.inc}}
+     {Year 4 Courses
+       \vskip 0.1in
+      Convener: ITO-Will-Determine\\
+      External Examiners: ITO-Will-Determine}{}
+   \ifthenelse{\equal{#1}{nonhons}}
+     {\vskip 0.2in
+      Convener: ITO-Will-Determine\\
+      External Examiner: ITO-Will-Determine}{}}}}
+
+\newcommand{\paperdate}[3]{\global\def\day{#1}\global\def\month{#2}\global\def\year{#3}}
+\newcommand{\papertimes}[2]{\global\def\timeofpaper{#1 to #2}}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Now, we first see if we're on an ITO machine and can load the
+%  proper status.tex.  If so, we do it and execute the corresponding
+%  \coursestatusfcn.
+%
+% Otherwise, based upon the value of courseid, we need to populate
+%  the title and type with basic mock-up data.
+%
+% This command must be called in the top-level exam document, after
+%  the courseid has been set.
+%
+% To do so: \initcoursedata
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\newcommand{\initcoursedata}{
+ \IfFileExists{\itostatuspath status.tex}
+  {
+   %
+   % If we're here, then we're on an ITO machine.
+   %
+
+   \input{\itostatuspath status.tex}
+
+   %
+   % We've loaded status.tex properly then, and can now execute
+   %  the corresponding \XXXdetails command.
+   %
+
+    \ifthenelse{\equal{\courseid}{anlp}}
+      {\anlpdetails}{}
+    \ifthenelse{\equal{\courseid}{aleone}}
+      {\aleonedetails}{}
+	\ifthenelse{\equal{\courseid}{adbs}}
+      {\adbsdetails}{}
+    \ifthenelse{\equal{\courseid}{av}}
+      {\avdetails}{}
+	\ifthenelse{\equal{\courseid}{apl}}
+      {\apldetails}{}
+    \ifthenelse{\equal{\courseid}{abs}}
+      {\absdetails}{}
+    \ifthenelse{\equal{\courseid}{agta}}
+      {\agtadetails}{}
+    \ifthenelse{\equal{\courseid}{ads}}
+      {\adsdetails}{}
+	\ifthenelse{\equal{\courseid}{ad}}
+	  {\addetails}{}
+    \ifthenelse{\equal{\courseid}{ar}}
+      {\ardetails}{}
+    \ifthenelse{\equal{\courseid}{asr}}
+      {\asrdetails}{}
+    \ifthenelse{\equal{\courseid}{bioone}}
+      {\bioonedetails}{}
+    \ifthenelse{\equal{\courseid}{biotwo}}
+      {\biotwodetails}{}
+    \ifthenelse{\equal{\courseid}{bdl}}
+      {\bdldetails}{}
+	 \ifthenelse{\equal{\courseid}{cqi}}
+      {\cqidetails}{}
+    \ifthenelse{\equal{\courseid}{copt}}
+      {\coptdetails}{}
+    \ifthenelse{\equal{\courseid}{ct}}
+      {\ctdetails}{}
+    \ifthenelse{\equal{\courseid}{ccs}}
+      {\ccsdetails}{}
+    \ifthenelse{\equal{\courseid}{cmc}}
+      {\cmcdetails}{}
+    \ifthenelse{\equal{\courseid}{ca}}
+      {\cadetails}{}
+    \ifthenelse{\equal{\courseid}{cav}}
+      {\cavdetails}{}
+    \ifthenelse{\equal{\courseid}{car}}
+      {\cardetails}{}
+    \ifthenelse{\equal{\courseid}{comn}}
+      {\comndetails}{}
+    \ifthenelse{\equal{\courseid}{cd}}
+      {\cddetails}{}
+    \ifthenelse{\equal{\courseid}{cg}}
+      {\cgdetails}{}
+    \ifthenelse{\equal{\courseid}{cn}}
+      {\cndetails}{}
+    \ifthenelse{\equal{\courseid}{cp}}
+      {\cpdetails}{}
+    \ifthenelse{\equal{\courseid}{cs}}
+      {\csdetails}{}
+	\ifthenelse{\equal{\courseid}{dme}}
+	  {\dmedetails}{}
+	\ifthenelse{\equal{\courseid}{dds}}
+	  {\ddsdetails}{}
+    \ifthenelse{\equal{\courseid}{dbs}}
+      {\dbsdetails}{}
+    \ifthenelse{\equal{\courseid}{dmmr}}
+      {\dmmrdetails}{}
+    \ifthenelse{\equal{\courseid}{dmr}}
+      {\dmrdetails}{}
+    \ifthenelse{\equal{\courseid}{ds}}
+      {\dsdetails}{}
+	\ifthenelse{\equal{\courseid}{epl}}
+	  {\epldetails}{}
+    \ifthenelse{\equal{\courseid}{es}}
+      {\esdetails}{}
+    \ifthenelse{\equal{\courseid}{exc}}
+      {\excdetails}{}
+    \ifthenelse{\equal{\courseid}{fv}}
+      {\fvdetails}{}
+    \ifthenelse{\equal{\courseid}{fnlp}}
+      {\fnlpdetails}{}
+    \ifthenelse{\equal{\courseid}{hci}}
+      {\hcidetails}{}
+    \ifthenelse{\equal{\courseid}{infonecg}}
+      {\infonecgdetails}{}
+    \ifthenelse{\equal{\courseid}{infonecl}}
+      {\infonecldetails}{}
+    \ifthenelse{\equal{\courseid}{infoneda}}
+      {\infonedadetails}{}
+    \ifthenelse{\equal{\courseid}{infonefp}}
+      {\infonefpdetails}{}
+    \ifthenelse{\equal{\courseid}{infonefpam}}
+      {\infonefpamdetails}{}
+    \ifthenelse{\equal{\courseid}{infonefppm}}
+      {\infonefppmdetails}{}
+    \ifthenelse{\equal{\courseid}{infoneop}}
+      {\infoneopdetails}{}
+    \ifthenelse{\equal{\courseid}{infoneopam}}
+      {\infoneopamdetails}{}
+    \ifthenelse{\equal{\courseid}{infoneoppm}}
+      {\infoneoppmdetails}{}
+    \ifthenelse{\equal{\courseid}{inftwoa}}
+      {\inftwoadetails}{}
+    \ifthenelse{\equal{\courseid}{inftwob}}
+      {\inftwobdetails}{}
+    \ifthenelse{\equal{\courseid}{inftwoccs}}
+      {\inftwoccsdetails}{}
+    \ifthenelse{\equal{\courseid}{inftwocse}}
+      {\inftwocsedetails}{}
+    \ifthenelse{\equal{\courseid}{inftwod}}
+      {\inftwoddetails}{}
+    \ifthenelse{\equal{\courseid}{iar}}
+      {\iardetails}{}
+    \ifthenelse{\equal{\courseid}{imc}}
+      {\imcdetails}{}
+    \ifthenelse{\equal{\courseid}{iotssc}}
+      {\iotsscdetails}{}
+    \ifthenelse{\equal{\courseid}{iqc}}
+      {\iqcdetails}{}
+    \ifthenelse{\equal{\courseid}{itcs}}
+      {\itcsdetails}{}
+    \ifthenelse{\equal{\courseid}{ivc}}
+      {\ivcdetails}{}
+    \ifthenelse{\equal{\courseid}{ivr}}
+      {\ivrdetails}{}
+    \ifthenelse{\equal{\courseid}{iaml}}
+      {\iamldetails}{}
+    \ifthenelse{\equal{\courseid}{lpt}}
+      {\lptdetails}{}
+    \ifthenelse{\equal{\courseid}{lpp}}
+      {\lppdetails}{}
+    \ifthenelse{\equal{\courseid}{mlpr}}
+      {\mlprdetails}{}
+    \ifthenelse{\equal{\courseid}{mt}}
+      {\mtdetails}{}
+	\ifthenelse{\equal{\courseid}{mi}}
+	  {\midetails}{}
+    \ifthenelse{\equal{\courseid}{nlu}}
+      {\nludetails}{}
+    \ifthenelse{\equal{\courseid}{nc}}
+      {\ncdetails}{}
+    \ifthenelse{\equal{\courseid}{nip}}
+      {\nipdetails}{}
+    \ifthenelse{\equal{\courseid}{os}}
+      {\osdetails}{}
+    \ifthenelse{\equal{\courseid}{pa}}
+      {\padetails}{}
+    \ifthenelse{\equal{\courseid}{pdiot}}
+      {\pdiotdetails}{}
+    \ifthenelse{\equal{\courseid}{ppls}}
+      {\pplsdetails}{}
+    \ifthenelse{\equal{\courseid}{pm}}
+      {\pmdetails}{}
+    \ifthenelse{\equal{\courseid}{pmr}}
+      {\pmrdetails}{}
+    \ifthenelse{\equal{\courseid}{pi}}
+      {\pidetails}{}
+    \ifthenelse{\equal{\courseid}{rc}}
+      {\rcdetails}{}
+    \ifthenelse{\equal{\courseid}{rl}}
+      {\rldetails}{}
+    \ifthenelse{\equal{\courseid}{rlsc}}
+      {\rlscdetails}{}
+    \ifthenelse{\equal{\courseid}{rss}}
+      {\rssdetails}{}
+	\ifthenelse{\equal{\courseid}{sp}}
+	  {\spdetails}{}
+    \ifthenelse{\equal{\courseid}{sws}}
+      {\swsdetails}{}
+	\ifthenelse{\equal{\courseid}{stn}}
+	  {\stndetails}{}
+    \ifthenelse{\equal{\courseid}{sapm}}
+      {\sapmdetails}{}
+    \ifthenelse{\equal{\courseid}{sdm}}
+      {\sdmdetails}{}
+    \ifthenelse{\equal{\courseid}{st}}
+      {\stdetails}{}
+    \ifthenelse{\equal{\courseid}{ttds}}
+      {\ttdsdetails}{}
+    \ifthenelse{\equal{\courseid}{tspl}}
+      {\tspldetails}{}
+
+  }
+  {
+   %
+   % If we're here, then we're on an exam preparer's machine.
+   % So, we're going to use their set \courseid to give some
+   %  nice mock-up values to the title and type text.
+   %
+
+    \ifthenelse{\equal{\courseid}{anlp}}
+      {\papertitle{INFR 11125 Accelerated Natural Language Processing}
+       \papertype{msc.inc}}{}
+    \ifthenelse{\equal{\courseid}{aleone}}
+      {\papertitle{Adaptive Learning Environments (Level 11)}
+       \papertype{inf4.inc}}{}
+	\ifthenelse{\equal{\courseid}{adbs}}
+      {\papertitle{Advanced Databases}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{av}}
+      {\papertitle{Advanced Vision (Level 11)}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{apl}}
+      {\papertitle{Advances in Programming Languages}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{abs}}
+      {\papertitle{Agent Based Systems}
+       \papertype{inf3.inc}}{}
+    \ifthenelse{\equal{\courseid}{agta}}
+      {\papertitle{Algorithmic Game Theory and its Applications}
+       \papertype{msc.inc}}{}
+    \ifthenelse{\equal{\courseid}{ads}}
+      {\papertitle{Algorithms and Data Structures}
+       \papertype{inf3.inc}}{}
+	\ifthenelse{\equal{\courseid}{ad}}
+	  {\papertitle{INFR11015 Applied Databases}
+	   \papertype{msc.inc}}{}
+    \ifthenelse{\equal{\courseid}{ar}}
+      {\papertitle{Automated Reasoning (Level 11)}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{asr}}
+      {\papertitle{Automatic Speech Recognition}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{bioone}}
+      {\papertitle{Bioinformatics 1}
+       \papertype{msc.inc}}{}
+    \ifthenelse{\equal{\courseid}{biotwo}}
+      {\papertitle{Bioinformatics 2}
+       \papertype{msc.inc}}{}
+    \ifthenelse{\equal{\courseid}{bdl}}
+      {\papertitle{INFR11144 Blockchains and Distributed Ledgers}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{cqi}}
+      {\papertitle{Categories and Quantum Informatics}
+       \papertype{msc.inc}}{}
+    \ifthenelse{\equal{\courseid}{copt}}
+      {\papertitle{Compiler Optimisation (Level 11)}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{ct}}
+      {\papertitle{Compiling Techniques}
+       \papertype{inf3.inc}}{}
+    \ifthenelse{\equal{\courseid}{ccs}}
+      {\papertitle{Computational Cognitive Science}
+       \papertype{inf3.inc}}{}
+    \ifthenelse{\equal{\courseid}{cmc}}
+      {\papertitle{Computational Complexity}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{ca}}
+      {\papertitle{Computer Algebra}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{cav}}
+      {\papertitle{Computer Animation and Visualisation (Level 11)}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{car}}
+      {\papertitle{Computer Architecture}
+       \papertype{inf3.inc}}{}
+    \ifthenelse{\equal{\courseid}{comn}}
+      {\papertitle{Computer Communications and Networks}
+       \papertype{inf3.inc}}{}
+    \ifthenelse{\equal{\courseid}{cd}}
+      {\papertitle{Computer Design}
+       \papertype{inf3.inc}}{}
+    \ifthenelse{\equal{\courseid}{cg}}
+      {\papertitle{Computer Graphics (Level 11)}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{cn}}
+      {\papertitle{Computer Networking (Level 11)}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{cp}}
+      {\papertitle{Computer Programming Skills and Concepts}
+       \papertype{nonhons.inc}}{}
+    \ifthenelse{\equal{\courseid}{cs}}
+      {\papertitle{Computer Security}
+       \papertype{inf3.inc}}{}
+	\ifthenelse{\equal{\courseid}{dds}}
+	  {\papertitle{INFR08024 Data, Design and Society}
+	   \papertype{nonhons.inc}}{}
+	\ifthenelse{\equal{\courseid}{dme}}
+	  {\papertitle{Data Mining and Exploration}
+	   \papertype{msc.inc}}{}
+    \ifthenelse{\equal{\courseid}{dbs}}
+      {\papertitle{Database Systems}
+       \papertype{inf3.inc}}{}
+    \ifthenelse{\equal{\courseid}{dmr}}
+      {\papertitle{Decision Making in Robots and Autonomous Agents}
+       \papertype{nonhons.inc}}{}
+    \ifthenelse{\equal{\courseid}{dmmr}}
+      {\papertitle{Discrete Mathematics and Mathematical Reasoning}
+       \papertype{nonhons.inc}}{}
+    \ifthenelse{\equal{\courseid}{ds}}
+      {\papertitle{Distributed Systems (Level 11)}
+       \papertype{inf4.inc}}{}
+	\ifthenelse{\equal{\courseid}{epl}}
+	  {\papertitle{INFR10061 Elements of Programming Languages}
+	   \papertype{inf3.inc}}{}
+    \ifthenelse{\equal{\courseid}{es}}
+      {\papertitle{Embedded Software}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{exc}}
+      {\papertitle{Extreme Computing}
+       \papertype{inf4.inc}}{}
+	\ifthenelse{\equal{\courseid}{fv}}
+      {\papertitle{Formal Verification}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{fnlp}}
+      {\papertitle{Foundations of Natural Language Processing}
+       \papertype{inf3.inc}}{}
+    \ifthenelse{\equal{\courseid}{hci}}
+      {\papertitle{Human-Computer Interaction (Level 11)}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{infonecg}}
+      {\papertitle{Informatics 1 --- Cognitive Science}
+       \papertype{nonhons.inc}}{}
+    \ifthenelse{\equal{\courseid}{infonecl}}
+      {\papertitle{Informatics 1 --- Computation \& Logic}
+       \papertype{nonhons.inc}}{}
+    \ifthenelse{\equal{\courseid}{infoneda}}
+      {\papertitle{Informatics 1 --- Data \& Analysis}
+       \papertype{nonhons.inc}}{}
+    \ifthenelse{\equal{\courseid}{infonefp}}
+      {\papertitle{Informatics 1 --- Functional Programming}
+       \papertype{nonhons.inc}}{}
+    \ifthenelse{\equal{\courseid}{infonefpam}}
+      {\papertitle{Informatics 1 --- Functional Programming}
+       \papertype{nonhons.inc}}{}
+    \ifthenelse{\equal{\courseid}{infonefppm}}
+      {\papertitle{Informatics 1 --- Functional Programming}
+       \papertype{nonhons.inc}}{}
+    \ifthenelse{\equal{\courseid}{infoneop}}
+      {\papertitle{Informatics 1 --- Object-Oriented Programming}
+       \papertype{nonhons.inc}}{}
+    \ifthenelse{\equal{\courseid}{infoneopam}}
+      {\papertitle{Informatics 1 --- Object-Oriented Programming}
+       \papertype{nonhons.inc}}{}
+    \ifthenelse{\equal{\courseid}{infoneoppm}}
+      {\papertitle{Informatics 1 --- Object-Oriented Programming}
+       \papertype{nonhons.inc}}{}
+    \ifthenelse{\equal{\courseid}{inftwoa}}
+      {\papertitle{Informatics 2A: Processing Formal and Natural Languages}
+       \papertype{nonhons.inc}}{}
+    \ifthenelse{\equal{\courseid}{inftwob}}
+      {\papertitle{Informatics 2B: Algorithms, Data Structures, Learning}
+       \papertype{nonhons.inc}}{}
+    \ifthenelse{\equal{\courseid}{inftwoccs}}
+      {\papertitle{Informatics 2C: Introduction to Computer Systems}
+       \papertype{nonhons.inc}}{}
+    \ifthenelse{\equal{\courseid}{inftwocse}}
+      {\papertitle{Informatics 2C: Introduction to Software Engineering}
+       \papertype{nonhons.inc}}{}
+    \ifthenelse{\equal{\courseid}{inftwod}}
+      {\papertitle{Informatics 2D: Reasoning and Agents}
+       \papertype{nonhons.inc}}{}
+  \ifthenelse{\equal{\courseid}{iar}}
+       {\papertitle{Intelligent Autonomous Robotics (Level 10)}
+       \papertype{inf4.inc}}{}
+	\ifthenelse{\equal{\courseid}{imc}}
+       {\papertitle{Introduction to Modern Cryptography}
+       \papertype{inf4.inc}}{}
+	\ifthenelse{\equal{\courseid}{iotssc}}
+       {\papertitle{Internet of Things Systems, Security, and the Cloud}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{iqc}}
+       {\papertitle{Introduction to Quantum Computing}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{itcs}}
+       {\papertitle{Introduction to Theoretical Computer Science}
+        \papertype{inf3.inc}}{}
+    \ifthenelse{\equal{\courseid}{ivc}}
+      {\papertitle{Image and Vision Computing}
+       \papertype{msc.inc}}{}
+    \ifthenelse{\equal{\courseid}{ivr}}
+      {\papertitle{Introduction to Vision and Robotics}
+       \papertype{inf3.inc}}{}
+    \ifthenelse{\equal{\courseid}{iaml}}
+      {\papertitle{Introductory Applied Machine Learning}
+       \papertype{inf3.inc}}{}
+    \ifthenelse{\equal{\courseid}{lpt}}
+      {\papertitle{Logic Programming --- Theory}
+       \papertype{inf3.inc}}{}
+    \ifthenelse{\equal{\courseid}{lpp}}
+      {\papertitle{Logic Programming --- Programming}
+       \papertype{inf3.inc}}{}
+    \ifthenelse{\equal{\courseid}{mlpr}}
+      {\papertitle{Machine Learning and Pattern Recognition}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{mt}}
+      {\papertitle{Machine Translation (Level 11)}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{mi}}
+      {\papertitle{INFR11079 Music Informatics}
+       \papertype{msc.inc}}{}
+    \ifthenelse{\equal{\courseid}{nlu}}
+      {\papertitle{Natural Language Understanding (Level 11)}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{nc}}
+      {\papertitle{Neural Computation}
+       \papertype{msc.inc}}{}
+    \ifthenelse{\equal{\courseid}{nip}}
+      {\papertitle{Neural Information Processing}
+       \papertype{msc.inc}}{}
+    \ifthenelse{\equal{\courseid}{os}}
+      {\papertitle{Operating Systems}
+       \papertype{inf3.inc}}{}
+    \ifthenelse{\equal{\courseid}{pa}}
+      {\papertitle{Parallel Architectures (Level 11)}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{pdiot}}
+      {\papertitle{Principles and Design of IoT Systems}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{ppls}}
+      {\papertitle{Parallel Programming Languages and Systems (Level 11)}
+       \papertype{inf4.inc}}{}
+	\ifthenelse{\equal{\courseid}{pm}}
+      {\papertitle{Performance Modelling}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{pmr}}
+      {\papertitle{Probabilistic Modelling and Reasoning}
+       \papertype{msc.inc}}{}
+    \ifthenelse{\equal{\courseid}{pi}}
+      {\papertitle{Professional Issues}
+       \papertype{inf3.inc}}{}
+	\ifthenelse{\equal{\courseid}{rc}}
+      {\papertitle{Randomness and Computation}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{rl}}
+      {\papertitle{Reinforcement Learning}
+       \papertype{msc.inc}}{}
+    \ifthenelse{\equal{\courseid}{rlsc}}
+      {\papetitle{Robot Learning and Sensorimotor Control}
+       \papertype{msc.inc}}{}
+    \ifthenelse{\equal{\courseid}{rss}}
+      {\papertitle{Robotics: Science and Systems}
+       \papertype{msc.inc}}{}
+	\ifthenelse{\equal{\courseid}{sp}}
+	  {\papertitle{INFR11098 Secure Programming}
+	   \papertype{inf4.inc}}{}
+	\ifthenelse{\equal{\courseid}{sws}}
+	  {\papertitle{INFR11104 Semantic Web Systems}
+	   \papertype{inf4.inc}}{}
+	\ifthenelse{\equal{\courseid}{stn}}
+	  {\papertitle{INFR11124 Social and Technological Networks}
+	   \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{sapm}}
+      {\papertitle{Software Architecture, Process and Management (Level 11)}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{sdm}}
+      {\papertitle{Software Design and Modelling}
+       \papertype{inf3.inc}}{}
+    \ifthenelse{\equal{\courseid}{st}}
+      {\papertitle{Software Testing}
+       \papertype{inf3.inc}}{}
+    \ifthenelse{\equal{\courseid}{ttds}}
+      {\papertitle{Text Technologies for Data Science}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{tspl}}
+      {\papertitle{Types and Semantics for Programming Languages}
+       \papertype{inf4.inc}}{}
+
+ %   \ifthenelse{\equal{\courseid}{XXX}}
+ %     { }{}
+
+ %
+ % Let's also do a mock-up date/time to make the exam preparer happy:
+ % (Aren't we sweet?)
+ %
+
+    \paperdate{1}{4}{2017}
+    \papertimes{00:00}{00:00}
+
+ %
+ % Also, we'll set the exam status to internal for the mock-up.
+ %
+
+    \internal
+
+  }}
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Now, we can build the appropriate rubric form and type.
+%
+% We set rubric type and form to alert values.  These will be over-
+%  written if the author has done things right.  Otherwise, they
+%  will provide good error messages to the author.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\setrubricform{Rubric Form has not been initialized.}
+\setrubrictype{Rubric type has not been initialized.}
+
+\newcommand{\initrubricdata}{
+
+ %
+ % We need to load both form and type data for the rubric.
+ %
+ % If we're on an ITO machine, we'll load it from the master path.
+ % If not, we'll setup some mock-up values.
+ %
+ % We only do this if the rubric is not custom, though.
+ %
+ % This section also defines \rubricqA, B and C.  These are initialised as empty definitions
+ % and then the correct text is added depending on the rubric selected
+ %
+ \def\rubricqA{}
+ \def\rubricqB{}
+ \def\rubricqC{}
+
+ \ifthenelse{\equal{\rubricid}{custom}}{}
+ {
+     %% HONS RUBRICS
+
+     \ifthenelse{\equal{\rubricid}{qu1_and_either_qu2_or_qu3}}{
+     \setrubrictype{
+         Answer QUESTION 1 and ONE other question. \\
+          \bigskip
+         Question 1 is COMPULSORY. If both QUESTION 2 and QUESTION 3 are answered, only QUESTION 2 will be marked. \\
+          \bigskip
+         All questions carry equal weight.\\
+	      \bigskip
+	     CALCULATORS MAY NOT BE USED IN THIS EXAMINATION \\
+         }
+
+         %% Additional command to be used for question 1.
+         \def\rubricqA{THIS QUESTION IS COMPULSORY}
+		 \def\rubricqB{ANSWER EITHER THIS QUESTION OR QUESTION 3}
+		 \def\rubricqC{ANSWER EITHER THIS QUESTION OR QUESTION 2}
+     }{}
+
+     \ifthenelse{\equal{\rubricid}{qu1_and_either_qu2_or_qu3_calc}}{
+     \setrubrictype{
+         Answer QUESTION 1 and ONE other question. \\
+	      \bigskip
+	     Question 1 is COMPULSORY. If both QUESTION 2 and QUESTION 3 are answered, only QUESTION 2 will be marked. \\
+	      \bigskip
+	     All questions carry equal weight.\\
+           \bigskip
+
+         CALCULATORS MAY BE USED IN THIS EXAMINATION \\
+         }
+
+         %% Additional command to be used for question 1.
+         \def\rubricqA{THIS QUESTION IS COMPULSORY}
+		 \def\rubricqB{ANSWER EITHER THIS QUESTION OR QUESTION 3}
+		 \def\rubricqC{ANSWER EITHER THIS QUESTION OR QUESTION 2}
+     }{}
+
+     \ifthenelse{\equal{\rubricid}{any_two_of_three}}{
+     \setrubrictype{
+         Answer any TWO of the three questions. If more than two questions are answered, only QUESTION 1 and QUESTION 2 will be marked.\\
+          \bigskip
+         All questions carry equal weight.\\
+	      \bigskip
+         CALCULATORS MAY NOT BE USED IN THIS EXAMINATION \\
+         }
+     }{}
+
+     \ifthenelse{\equal{\rubricid}{any_two_of_three_calc}}{
+     \setrubrictype{
+	     Answer any TWO of the three questions. If more than two questions are answered, only QUESTION 1 and QUESTION 2 will be marked.\\
+	      \bigskip
+         All questions carry equal weight.\\
+          \bigskip
+         CALCULATORS MAY BE USED IN THIS EXAMINATION \\
+         }
+     }{}
+
+     \ifthenelse{\equal{\rubricid}{infone}}{
+     \setrubrictype{
+	     \begin{enumerate}
+	     \item Note that ALL QUESTIONS ARE COMPULSORY.
+	     \item DIFFERENT QUESTIONS MAY HAVE DIFFERENT NUMBERS OF TOTAL MARKS.
+	           Take note of this in allocating time to questions.
+	     \item CALCULATORS MAY NOT BE USED IN THIS EXAMINATION.
+	     \end{enumerate}
+         }
+     }{}
+
+	 \ifthenelse{\equal{\rubricid}{infone_calcs}}{
+     \setrubrictype{
+	     \begin{enumerate}
+         \item Note that ALL QUESTIONS ARE COMPULSORY.
+         \item DIFFERENT QUESTIONS MAY HAVE DIFFERENT NUMBERS OF TOTAL MARKS.
+               Take note of this in allocating time to questions.
+         \item CALCULATORS MAY BE USED IN THIS EXAMINATION.
+         \end{enumerate}
+         }
+     }{}
+
+     \ifthenelse{\equal{\rubricid}{infone_openbook}}{
+     \setrubrictype{
+         \begin{enumerate}
+         \item Note that ALL QUESTIONS ARE COMPULSORY.
+         \item DIFFERENT QUESTIONS MAY HAVE DIFFERENT NUMBERS OF TOTAL MARKS.
+               Take note of this in allocating time to questions.
+         \item This is an OPEN BOOK examination: notes and printed material are allowed,
+               but no electronic devices or electronic media.
+         \end{enumerate}
+         }
+     }{}
+
+ }
+}
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Now, we can build the title page.  This command must be called
+%  from the top-level exam document.
+%
+% To do so: \examtitlepage
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+\newcommand{\examtitlepage}{
+
+\initrubricdata
+
+\status
+
+\thispagestyle{header}
+\begin{center}
+ {UNIVERSITY OF EDINBURGH}
+ \vskip 0.1in
+ {COLLEGE OF SCIENCE AND ENGINEERING}
+ \vskip 0.1in
+ {SCHOOL OF INFORMATICS}
+ \vskip 0.5in
+
+\begin{bf}
+{\nameofpaper}
+
+\begin{small}
+\vskip 0.5in
+{\today} \\
+\vskip 0.2in
+{\timeofpaper}
+\vskip 0.75in
+\end{small}
+
+{INSTRUCTIONS TO CANDIDATES} \\
+\bigskip\bigskip
+
+\rubrictype
+\end{bf}
+
+\vskip 0.5in
+
+\begin{small}
+{\typeofpaper}
+\end{small}
+
+\vskip 0.5in
+THIS EXAMINATION WILL BE MARKED ANONYMOUSLY
+
+\end{center}
+
+\setcounter{page}{0}
+\newpage
+
+\status
+}
diff --git a/courses/tspl/2018/tspl2018.agda-lib b/courses/tspl/2018/tspl2018.agda-lib
new file mode 100644
index 00000000..8c72811e
--- /dev/null
+++ b/courses/tspl/2018/tspl2018.agda-lib
@@ -0,0 +1,3 @@
+name: tspl
+depend: standard-library plfa
+include: .
diff --git a/tspl/tspl.md b/courses/tspl/2018/tspl2018.md
similarity index 80%
rename from tspl/tspl.md
rename to courses/tspl/2018/tspl2018.md
index f3f3da14..70208680 100644
--- a/tspl/tspl.md
+++ b/courses/tspl/2018/tspl2018.md
@@ -1,7 +1,7 @@
 ---
 title     : "TSPL: Course notes"
 layout    : page
-permalink : /TSPL/
+permalink : /TSPL/2018/
 ---
 
 ## Staff
@@ -97,13 +97,13 @@ Lectures take place Monday, Wednesday, and Friday in AT 7.02. (Moved from AT 5.0
 
 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)
+* [Assignment 1](/TSPL/2018/Assignment1/) cw1 due 4pm Thursday 4 October (Week 3)
+* [Assignment 2](/TSPL/2018/Assignment2/) cw2 due 4pm Thursday 18 October (Week 5)
+* [Assignment 3](/TSPL/2018/Assignment3/) cw3 due 4pm Thursday 1 November (Week 7)
+* [Assignment 4](/TSPL/2018/Assignment4/) cw4 due 4pm Thursday 15 November (Week 9)
+* [Assignment 5](/courses/tspl/2018/Mock1.pdf) cw5 due 4pm Thursday 22 November (Week 10)
   <br />
-  Use file [Exam][Exam]. Despite the rubric, do **all three questions**.
+  Use file [Exam](/TSPL/2018/Exam/). Despite the rubric, do **all three questions**.
 
 
 Assignments are submitted by running
@@ -114,5 +114,5 @@ 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).
+Here is the text of the [second mock](/courses/tspl/2018/Mock2.pdf)
+and the exam [instructions](/courses/tspl/2018/Instructions.pdf).
diff --git a/highlight.sh b/highlight.sh
index f00e6381..4dcff164 100755
--- a/highlight.sh
+++ b/highlight.sh
@@ -9,18 +9,27 @@ OUT="$1"
 OUT_DIR="$(dirname $OUT)"
 shift
 
+# Extract the module name from the Agda file
+# NOTE: this fails if there is more than a single space after 'module'
+MOD_NAME=`grep -oP -m 1 "(?<=^module )(\\S+)(?=\\s+(\\S+\\s+)*where)" "$SRC"`
+
 # Create temporary directory and compute path to output of `agda --html`
-# NOTE: this assumes $OUT is equivalent to out/ plus the module path
 HTML_DIR="$(mktemp -d)"
-HTML="${OUT#out/}"
-HTML="/${HTML//\//.}"
-HTML="$HTML_DIR/$HTML"
+SRC_EXT="$(basename $SRC)"
+SRC_EXT="${SRC_EXT##*.}"
+HTML="$HTML_DIR/$MOD_NAME.$SRC_EXT"
 
 # Highlight Syntax using Agda
 set -o pipefail \
    && agda --html --html-highlight=code --html-dir="$HTML_DIR" "$SRC" "$@" \
     | sed '/^Generating.*/d; /^Warning\: HTML.*/d; /^reached from the.*/d; /^\s*$/d'
 
+# Check if the highlighted file was successfully generated
+if [[ ! -f "$HTML" ]]; then
+    echo "File not generated: $FILE"
+    exit 1
+fi
+
 # Add source file to the Jekyll metadata
 sed -i "1 s|---|---\nsrc: $SRC|" "$HTML"
 
diff --git a/index.md b/index.md
index bd9dbcac..4e2e43d6 100644
--- a/index.md
+++ b/index.md
@@ -49,12 +49,12 @@ Pull requests are encouraged.
 
   - Courses taught from the textbook:
     * Philip Wadler, University of Edinburgh,
-      [2018](/TSPL/)
+      [2018](/TSPL/2018/)
     * David Darais, University of Vermont,
       [2018](http://david.darais.com/courses/fa2018-cs295A/)
     * John Leo, Google Seattle, 2018--2019 
     * Philip Wadler, Pontifícia Universidade Católica do Rio de Janeiro (PUC-Rio),
-      [2019](/PUC/)
+      [2019](/PUC/2019/)
   - A paper describing the book appeared in [SBMF][sbmf]
 
 [wen]: https://github.com/wenkokke
diff --git a/tspl/Assignments.lagda.md b/tspl/Assignments.lagda.md
deleted file mode 100644
index bc9491ea..00000000
--- a/tspl/Assignments.lagda.md
+++ /dev/null
@@ -1,164 +0,0 @@
----
-title     : "Assignments: Summary of all assignments"
-layout    : page
-permalink : /Assignments/
----
-
-## Assignments
-
-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 without a label are optional, and may be done if you want
-some extra practice.
-
-* [Assignment 1][Assignment1] Due 4pm Thursday 4 October (Week 3)
-
-  + Naturals
-    - `seven`
-    - `+-example`
-    - `*-example`
-    - `_^_` (recommended)
-    - `∸-examples` (recommended)
-    - `Bin` (stretch)
-
-  + Induction
-    - `operators`
-    - `finite-+-assoc` (stretch)
-    - `+-swap` (recommended)
-    - `*-distribʳ-+` (recommended)
-    - `*-assoc` (recommended)
-    - `*-comm`
-    - `0∸n≡n`
-    - `∸-+-assoc`
-    - `Bin-laws` (stretch)
-
-  + Relations
-    - `orderings`
-    - `≤-antisym-cases`
-    - `*-mono-≤` (stretch)
-    - `<-trans` (recommended)
-    - `trichotomy`
-    - `+-mono-<`
-    - `≤-iff-<` (recommended)
-    - `<-trans-revisited`
-    - `o+o≡e` (recommended)
-    - `Bin-predicates` (stretch)
-
-* [Assignment 2][Assignment2]. Due 4pm Thursday 18 October (Week 5)
-
-  + Equality
-    - `≤-reasoning` (stretch)
-
-  + Isomorphism
-    - `≃-implies-≲`
-    - `_⇔_` (recommended)
-    - `Bin-embedding` (stretch)
-
-  + Connectives
-    - `⇔≃×` (recommended)
-    - `⊎-comm` (recommended)
-    - `⊎-assoc`
-    - `⊥-identityˡ` (recommended)
-    - `⊥-identityʳ`
-    - `⊎-weak-×` (recommended)
-    - `⊎×-implies-×⊎`
-
-  + Negation
-    - `<-irreflexive` (recommended)
-    - `trichotomy`
-    - `⊎-dual-×` (recommended)
-    - `Classical` (stretch)
-    - `Stable` (stretch)
-
-  + Quantifiers
-    - `∀-distrib-×` (recommended)
-    - `⊎∀-implies-∀⊎`
-    - `∃-distrib-⊎` (recommended)
-    - `∃×-implies-×∃`
-    - `∃-even-odd`
-    - `∃-+-≤`
-    - `∃¬-implies-¬∀` (recommended)
-    - `Bin-isomorphism` (stretch)
-
-  + Decidable
-    - `_<?_` (recommended)
-    - `_≡ℕ?_`
-    - `erasure`
-    - `iff-erasure` (recommended)
-
-* Assignment 3. Due 4pm Thursday 1 November (Week 7)
-
-  + Lists
-    - `reverse-++-commute` (recommended)
-    - `reverse-involutive` (recommended)
-    - `map-compose`
-    - `map-++-commute`
-    - `map-Tree`
-    - `product` (recommended)
-    - `fold-++` (recommended)
-    - `map-is-foldr`
-    - `fold-Tree`
-    - `map-is-fold-Tree`
-    - `sum-downFrom` (stretch)
-    - `foldl`
-    - `foldr-monoid-foldl`
-    - `Any-++-⇔` (recommended)
-    - `All-++-≃` (stretch)
-    - `¬Any≃All¬` (stretch)
-    - `any?` (stretch)
-    - `filter?` (stretch)
-
-  + Lambda
-    - `mul` (recommended)
-    - `primed` (stretch)
-    - `_[_:=_]′` (stretch)
-    - `—↠≃—↠′`
-    - `plus-example`
-    - `mul-type` (recommended)
-
-  + Properties
-    - `Progress-≃`
-    - `progress′`
-    - `value?` (recommended)
-    - `subst′` (stretch)
-    - `mul-example` (recommended)
-    - `progress-preservation`
-    - `subject-expansion`
-    - `stuck`
-    - `unstuck` (recommended)
-
-* Assignment 4. Due 4pm Thursday 15 November (Week 9)
-
-
-  + DeBruijn
-    - `mul` (recommended)
-    - `V¬—→`
-    - `mul-example` (recommended)
-
-  + More
-    - `More` (recommended)
-
-  + Bisimulation
-    - `_†`
-    - `~val⁻¹`
-    - `sim⁻¹`
-    - `products`
-
-  + Inference
-    - `bidirectional-ps` (recommended)
-    - `bidirectional-rest` (stretch)
-    - `inference-p` (recommended)
-    - `inference-rest` (stretch)
-
-  + Untyped
-    - `Type≃⊤`
-    - `Context≃ℕ`
-    - `variant-1` (recommended)
-    - `variant-2`
-    - `2+2≡four` (recommended)
-    - `encode-more` (stretch)
-
-* Assignment 5. Due 4pm Thursday 22 November (Week 10)
diff --git a/tspl/first-mock.pdf b/tspl/first-mock.pdf
deleted file mode 100644
index 46f859d9..00000000
Binary files a/tspl/first-mock.pdf and /dev/null differ
diff --git a/tspl/instructions.pdf b/tspl/instructions.pdf
deleted file mode 100644
index 0eb17918..00000000
Binary files a/tspl/instructions.pdf and /dev/null differ
diff --git a/tspl/second-mock.pdf b/tspl/second-mock.pdf
deleted file mode 100644
index b066b1ac..00000000
Binary files a/tspl/second-mock.pdf and /dev/null differ