diff --git a/papers/hatra23/bibliography.bib b/papers/hatra23/bibliography.bib
index 067bf967..3fbae85e 100644
--- a/papers/hatra23/bibliography.bib
+++ b/papers/hatra23/bibliography.bib
@@ -1,6 +1,6 @@
 @InProceedings{BFJ21:GoalsLuau,
   author = 	 {L. Brown and A. Friesen and A. S. A. Jeffrey},
-  title = 	 {Goals of the Luau Type System},
+  title = 	 {Position Paper: Goals of the Luau Type System},
   booktitle =	 {Proc. Human Aspects of Types and Reasoning Assistants},
   year =	 {2021},
   url =          {https://asaj.org/papers/hatra21.pdf},
diff --git a/papers/hatra23/hatra23.pdf b/papers/hatra23/hatra23.pdf
index 32e83b9b..b750ecae 100644
Binary files a/papers/hatra23/hatra23.pdf and b/papers/hatra23/hatra23.pdf differ
diff --git a/papers/hatra23/hatra23.tex b/papers/hatra23/hatra23.tex
index 72e1f181..1d73ee53 100644
--- a/papers/hatra23/hatra23.tex
+++ b/papers/hatra23/hatra23.tex
@@ -49,7 +49,7 @@ error reporting). Roblox has hundreds of millions of users, and
 millions of creators, ranging from children learning to program for
 the first time to professional development studios.
 
-In HATRA 2021, we presented \emph{The Goals Of The Luau Type
+In HATRA 2021, we presented a position paper on the \emph{Goals Of The Luau Type
 System}~\cite{BFJ21:GoalsLuau}, describing the human factors issues
 with designing a type system for a language with a heterogeneous
 developer community. The design flows from the needs of the different
@@ -103,7 +103,7 @@ We have now released an implementation of semantic subtyping, which does not suf
 See our technical blog for more details~\cite{Jef22:SemanticSubtyping}.
 
 Rather than the gradual typing approach
-of~\cite{ST07:GradualTyping}, which uses \emph{consistent
+of Siek and Taha~\cite{ST07:GradualTyping}, which uses \emph{consistent
 subtyping} where $\ANY \lesssim T \lesssim \ANY$ for any type $T$, we
 adopt an approach based on \emph{error suppression}, where $\ANY$ is
 an error-suppressing type, and any failures of subtyping involving