From 8ecfadb94e30e28a3f7ae3fb717a730ac4d19240 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= <daniel.hillerstrom@ed.ac.uk>
Date: Tue, 18 May 2021 08:04:20 +0100
Subject: [PATCH] Fix Ref macro

---
 macros.tex |  1 +
 thesis.tex | 28 ++++++++++++++--------------
 2 files changed, 15 insertions(+), 14 deletions(-)

diff --git a/macros.tex b/macros.tex
index e33dae9..8184e19 100644
--- a/macros.tex
+++ b/macros.tex
@@ -77,6 +77,7 @@
 \newcommand{\Inl}{\keyw{inl}}
 \newcommand{\Inr}{\keyw{inr}}
 \newcommand{\Thunk}{\lambda \Unit.}
+\newcommand{\PCFRef}{\keyw{ref}}
 
 \newcommand{\Pre}[1]{\mathsf{Pre}(#1)}
 \newcommand{\Abs}{\mathsf{Abs}}
diff --git a/thesis.tex b/thesis.tex
index 99579d3..1c7b80f 100644
--- a/thesis.tex
+++ b/thesis.tex
@@ -1163,20 +1163,20 @@ handlers.
 %
 \dhil{Definition of (typed) programming language, conservative extension, macro-expressiveness~\cite{Felleisen90,Felleisen91}}
 
-\chapter{State of effectful programming}
-\label{ch:related-work}
+% \chapter{State of effectful programming}
+% \label{ch:related-work}
 
-% \section{Type and effect systems}
-% \section{Monadic programming}
-\section{Golden age of impurity}
-\section{Monadic enlightenment}
-\dhil{Moggi's seminal work applies the notion of monads to effectful
-  programming by modelling effects as monads. More importantly,
-  Moggi's work gives a precise characterisation of what's \emph{not}
-  an effect}
-\section{Direct-style revolution}
+% % \section{Type and effect systems}
+% % \section{Monadic programming}
+% \section{Golden age of impurity}
+% \section{Monadic enlightenment}
+% \dhil{Moggi's seminal work applies the notion of monads to effectful
+%   programming by modelling effects as monads. More importantly,
+%   Moggi's work gives a precise characterisation of what's \emph{not}
+%   an effect}
+% \section{Direct-style revolution}
 
-\subsection{Monadic reflection: best of both worlds}
+% \subsection{Monadic reflection: best of both worlds}
 
 \chapter{Continuations}
 \label{ch:continuations}
@@ -15868,11 +15868,11 @@ be modified.
 
 We have in mind an extension $\BCalcS$ of $\BCalc$ with ML-style
 reference cells: we extend our grammar for types with a reference type
-($\Ref~A$), and that for computation terms with forms for creating
+($\PCFRef~A$), and that for computation terms with forms for creating
 references ($\keyw{letref}\; x = V\; \In\; N$), dereferencing ($!x$),
 and destructive update ($x := V$), with the familiar typing rules.  We
 also add a new kind of value, namely \emph{locations} $l^A$, of type
-$\Ref~A$. We adopt a basic Scott-Strachey~\citeyearpar{ScottS71} model
+$\PCFRef~A$. We adopt a basic Scott-Strachey~\citeyearpar{ScottS71} model
 of store: a location is a natural number decorated with a type, and
 the execution of a stateful program allocates locations in the order
 $0,1,2,\ldots$, assigning types to them as it does so. A \emph{store}