fix some typos pointed out in reviews

paper/gtt.tex

@@ -7,7 +7,7 @@
 %% For single-blind review submission, w/ CCS and ACM Reference
 %\documentclass[acmsmall,review]{acmart}\settopmatter{printfolios=true}
 %% For final camera-ready submission, w/ required CCS and ACM Reference
-%\documentclass[acmsmall]{acmart}\settopmatter{}
+\documentclass[acmsmall]{acmart}\settopmatter{}
 
 \newif\ifshort
 \newif\iflong
@@ -569,15 +569,20 @@ The cast reductions that we show satisfy all three constraints are
 those given by the ``lazy cast semantics''~\cite{findler-felleisen02,siek+09designspace}.  
 %
 For instance, a transient semantics, where only the top-level
-connectives are checked, violates $\eta$: ${x : A_1 \times (A_2 \times A_3)}$ $\letXbeYinZ x
-{(x_1,(x_2,x_3))} 0$ is not equivalent to $0$, but this is provable in
-GTT using the $\eta$ principle for $\times$.  Next, in a typical CBV
-``eager cast semantics'' the $\beta, \eta$ principles for all of the
-eager datatypes ($0, +, 1, \times$, lists, etc.) will be satisfied, but
-the $\eta$ principle for the function type $\to$ is violated, i.e.,
-there are values $V : A \to A'$ for which $V \neq \lambda x:A. V x $.
-%
-Thus, we argue that ``eager'' cast semantics is in fact overly eager: in
+connectives are checked, violates $\eta$ for strict pairs:
+\begin{small}
+  \[ {x : A_1 \times (A_2 \times A_3)} \vdash \letXbeYinZ x {(x_1,(x_2,x_3))} 0 \neq 0 \]
+\end{small}
+because the top-level connectives of $A_2, A_3$ are checked when the
+pattern match is introduced.
+%
+Next, in a typical CBV ``eager cast semantics'' the $\beta, \eta$
+principles for all of the eager datatypes ($0, +, 1, \times$, lists,
+etc.) will be satisfied, but the $\eta$ principle for the function
+type $\to$ is violated, i.e., there are values $V : A \to A'$ for
+which $V \neq \lambda x:A. V x $.
+%
+We argue that ``eager'' cast semantics is in fact overly eager: in
 its effort to find bugs faster than ``lazy'' semantics it disables the
 very program equivalences that gradual typing should provide.
 
@@ -1535,8 +1540,11 @@ like an upcast, and dually for the downcast, so this formulation
 implies the original formulation above.
 
 We justify this design in two ways in the remainder of the paper.  In
-Section~\ref{sec:contract}, we show how to implement casts by a contract
-translation to CBPV in such a way that it is true.  However, one goal of
+Section~\ref{sec:contract}, we show how to implement casts by a
+contract translation to CBPV where upcasts are complex values and
+downcasts are complex stacks.
+%
+However, one goal of
 GTT is to be able to prove things about many gradually typed languages
 at once, by giving different models, so one might wonder whether this
 design rules out potential models where casts are effectful.  In
@@ -1923,7 +1931,7 @@ heterogeneous way, which includes congruence $\Gamma \ltdyn \Gamma'
     \framebox{Error Properties}
     \qquad
     \inferrule{ \Gamma' \mid \cdot \vdash M' : \u B' }
-              { \Gamma \ltdyn \Gamma' \mid \cdot \vdash \err \ltdyn M : \u B \ltdyn \u B'}
+              { \Gamma \ltdyn \Gamma' \mid \cdot \vdash \err \ltdyn M' : \u B \ltdyn \u B'}
     \qquad
     \inferrule { \Gamma \mid x : \u B \vdash S : \u B'}
                {\Gamma \mid \cdot \vdash S[\err_{\u B}] \ltdyn \err_{\u{B'}} : \u B'}
@@ -3795,7 +3803,7 @@ In GTT$_G$ it is admissible that
   satisfying the universal property of a downcast
 \item for all $\u B \ltdyn \u B'$ there is a complex
   stack $\defdncast{\u B}{\u B'}$ satisfying the universal property of a
-  downcast and a complex value $\defdncast{U \u B}{U \u B'}$ satisfying
+  downcast and a complex value $\defupcast{U \u B}{U \u B'}$ satisfying
   the universal property of an upcast.
 \end{enumerate}
 \end{lemma}
@@ -4941,7 +4949,7 @@ interpretation.
       \bullet : \u F \dynv \vdash \sdncast{\u F \dynv}{\u F\dynv} &=& \bullet\\
       x : \sem{G} \vdash \sem{\upcast{G}{\dynv}} & = & \rho_{up}(G)\\
       \bullet : \u F \dynv \vdash \sdncast{\u F G}{\u F\dynv} &=& \rho_{dn}(G)\\
-      x : \sem{A} \vdash \sem{\upcast{A}{\dynv}} & = & \sem{\upcast{A}{\lfloor A \rfloor}}[{\sem{\upcast{G}{\dynv}}}/x]\\
+      x : \sem{A} \vdash \sem{\upcast{A}{\dynv}} & = & \sem{\upcast{\lfloor A \rfloor}{\dynv}}[{\sem{\upcast{A}{\lfloor A \rfloor}}}/x]\\
       \bullet: \u F\dynv \vdash \sdncast{A}{\dynv} &=& \sdncast{A}{\floor A}[{\sdncast{\floor A}{\dynv}}]\\
 \iflong
       x : \sem{A_1} + \sem{A_2} \vdash \sem{\upcast{A_1 + A_2}{A_1' + A_2'}}

popl19/corrections.org

 * Typos
-  - 111: missing a turnstile, would be better to have on its own line.
-  - 687: one of these should be an upcast
-  - l475: "that it is true" that what is true?
-  - l559: the rule err <= M uses M below and M' above.
-  - l898: G should be floor A
+  - [X] 111: missing a turnstile, would be better to have on its own line.
+  - [X] 687: one of these should be an upcast
+  - [X] l475: "that it is true" that what is true?
+  - [X] l559: the rule err <= M uses M below and M' above.
+  - [X] l898: G should be floor A
 * Clarity
   - multiple reviewers: there isn't a "we did this" part of the intro
   - numeric citations as nouns: L1025 and "elsewhere".