From 27675151806af69526bd9dbe3ef5bc3aeaf5efe5 Mon Sep 17 00:00:00 2001
From: John Wickerson <j.wickerson@imperial.ac.uk>
Date: Mon, 13 Sep 2021 08:10:44 +0000
Subject: Update on Overleaf.

---
 main.tex       |  2 +-
 proof.tex      |  2 +-
 references.bib | 20 --------------------
 3 files changed, 2 insertions(+), 22 deletions(-)

diff --git a/main.tex b/main.tex
index 2206e06..f9c72b5 100644
--- a/main.tex
+++ b/main.tex
@@ -217,7 +217,7 @@
   We would like to thank Sandrine Blazy, Jianyi Cheng, Alastair Donaldson, Andreas Lööw, and the
   anonymous reviewers for their helpful feedback.  This work was financially supported by the EPSRC
   via the Research Institute for Verified Trustworthy Software Systems (VeTSS) and the IRIS
-  Programme Grant (EP/R006865/1) as well as EP/P010040/1.
+  Programme Grant (EP/R006865/1).
 \end{acks}
 
 %% Bibliography
diff --git a/proof.tex b/proof.tex
index 1654583..d4df35c 100644
--- a/proof.tex
+++ b/proof.tex
@@ -45,7 +45,7 @@ The forward simulation from 3AC to HTL is stated in Lemma~\ref{lemma:htl} (Secti
 As HTL is quite far removed from 3AC, this first translation is the most involved and therefore requires a larger proof, because the translation from 3AC instructions to Verilog statements needs to be proven correct in this step.  In addition to that, the semantics of HTL are also quite different to the 3AC semantics. Instead of defining small-step semantics for each construct in Verilog, the semantics are defined over one clock cycle and mirror the semantics defined for Verilog.  Lemma~\ref{lemma:htl} shows the result that needs to be proven in this subsection.
 
 \begin{lemma}[Forward simulation from 3AC to HTL]\label{lemma:htl}
-  We write \texttt{tr\_htl} for the translation from 3AC to HTL.
+  Writing \texttt{tr\_htl} for the translation from 3AC to HTL, we have:
   \begin{equation*}
     \forall c, h, B \in \texttt{Safe},\quad \yhfunction{tr\_htl} (c) = \yhconstant{OK} (h) \land c \Downarrow B \implies h \Downarrow B.
   \end{equation*}
diff --git a/references.bib b/references.bib
index b183298..c1e979a 100644
--- a/references.bib
+++ b/references.bib
@@ -734,26 +734,6 @@ year = {2020},
 }
 
 
-  author          = {Zhao, Jianzhou and Nagarakatte, Santosh and Martin, Milo M.K. and Zdancewic,
-                  Steve},
-  title           = {Formalizing the {LLVM} Intermediate Representation for Verified Program
-                  Transformations},
-  journal         = {SIGPLAN Not.},
-  volume          = {47},
-  number          = {1},
-  pages           = {427-440},
-  year            = {2012},
-  doi             = {10.1145/2103621.2103709},
-  url             = {https://doi.org/10.1145/2103621.2103709},
-  address         = {New York, NY, USA},
-  issn            = {0362-1340},
-  issue_date      = {January 2012},
-  keywords        = {LLVM, memory safety, Coq},
-  month           = jan,
-  numpages        = {14},
-  publisher       = {ACM},
-}
-
 @inproceedings{hwang99_fsmd,
   author          = {Hwang, Enoch and Vahid, Frank and Hsu, Yu-Chin},
   title           = {FSMD functional partitioning for low power},
-- 
cgit