diff --git a/papers/hatra21/hatra21.pdf b/papers/hatra21/hatra21.pdf
index b398b1c1..5b1b5c25 100644
Binary files a/papers/hatra21/hatra21.pdf and b/papers/hatra21/hatra21.pdf differ
diff --git a/papers/hatra21/hatra21.tex b/papers/hatra21/hatra21.tex
index 3e6b5bfa..d3e05fad 100644
--- a/papers/hatra21/hatra21.tex
+++ b/papers/hatra21/hatra21.tex
@@ -28,20 +28,20 @@
 
 \title{Position Paper: Some Goals of the Luau Type System}
 
-\author{Lily Brown}
-\author{Andy Friesen}
-\author{Alan Jeffrey}
-\affiliation{
-  \institution{Roblox}
-  \city{San Mateo}
-  \state{CA}
-  \country{USA}
-}
+%% \author{Lily Brown}
+%% \author{Andy Friesen}
+%% \author{Alan Jeffrey}
+%% \affiliation{
+%%   \institution{Roblox}
+%%   \city{San Mateo}
+%%   \state{CA}
+%%   \country{USA}
+%% }
 
 \begin{abstract}
   Luau is the scripting language that powers user-generated experiences on the
-  Roblox platform. It is a statically-typed language with type inference based
-  on the dynamically-typed Lua language. These types are used for providing
+  Roblox platform. It is a statically-typed language, based on the
+  dynamically-typed Lua language, with type inference. These types are used for providing
   editor assistance in Roblox Studio, the IDE for authoring Roblox experiences.
   Due to Roblox's uniquely heterogeneous developer community, Luau must operate
   in a somewhat different fashion than a traditional statically-typed language.
@@ -56,8 +56,8 @@
 The Roblox~\cite{Roblox} platform allows anyone to create shared,
 immersive, 3D experiences.  As of July 2021, there are
 approximately 20~million experiences available on Roblox, created
-by 8~million developers.  Roblox creators are often young. For
-example, there are over 200~Roblox kids' coding camps in 65~countries
+by 8~million developers.  Roblox creators are often young: there are
+over 200~Roblox kids' coding camps in 65~countries
 listed by the company as education resources~\cite{AllEducators}.
 The Luau programming language~\cite{Luau} is the scripting language
 used by creators of Roblox experiences. Luau is derived from the Lua
@@ -74,8 +74,8 @@ these goals differ from traditional type systems' goals.
 
 Quoting a Roblox 2020 report \cite{RobloxDevelopers}:
 \begin{itemize}
-\item Adopt Me! now has over 10 billion plays and surpassed 1.6 million concurrent users earlier this year.
-\item Piggy, launched in January 2020, has close to 5 billion visits in just over six months.
+\item \emph{Adopt Me!} now has over 10 billion plays and surpassed 1.6 million concurrent users earlier this year.
+\item \emph{Piggy}, launched in January 2020, has close to 5 billion visits in just over six months.
 \item There are now 345,000 developers on the platform who are monetizing their games.
 \end{itemize}
 This demonstrates the heterogeneity of the Roblox developer community:
@@ -110,9 +110,9 @@ and multiplayer are all immediately accessible to creators.
 \end{figure}
 
 At some point during experience design, the experience creator has a need
-which can't be met by the physics engine alone, such as ``The stairs should
+that can't be met by the physics engine alone, such as ``the stairs should
 light up when a player walks on them'' or ``a firework is set off
-every few seconds.'' At this point they will discover the script
+every few seconds.'' At this point, they will discover the script
 editor, seen in Fig.~\ref{fig:studio}(b).
 
 This onboarding experience is different from many initial exposures to
@@ -148,7 +148,7 @@ resulting in an array of techniques for establishing safety results,
 surveyed for example in~\cite{TAPL}. Supporting code planning and
 refactoring are some of the goals of \emph{type-driven
 development}~\cite{TDDIdris} under the slogan ``type, define,
-refine''.  For example, a common use of type-driven development is renaming a
+refine''.  A common use of type-driven development is renaming a
 property, which is achieved by changing the name in one place,
 and then fixing the resulting type errors---once the type system stops
 reporting errors, the refactoring is complete.
@@ -276,7 +276,7 @@ when executed.
 
 On the face of it, this is undecidable, since a program such as
 $(\IF f() \THEN \ERROR \END)$ will produce a runtime error when $f()$ is
-$\TRUE$, but we can aim for a weaker property, that all flagged code
+$\TRUE$, but we can aim for a weaker property: that all flagged code
 is either dead code or will produce an error. Either of these is a
 defect, so deserves flagging, even if the tool does not know
 which reason applies.