diff --git a/paper/abstract.tex b/paper/abstract.tex
index e876b0d08f27d74f2c580e693cc750a63c8e238d..7d26f3cff886e05790b2c34525a6fdbba5ebc10d 100644
--- a/paper/abstract.tex
+++ b/paper/abstract.tex
@@ -1,12 +1,11 @@
 Gradually typed languages are designed to support both dynamically typed and
 statically typed programming styles while preserving the benefits of each.
-Gradual type soundness theorems for these languages are aimed at showing that 
-type-based reasoning is preserved when moving from the fully static setting to a
-gradual one. But gradual type soundness does not imply that type-based
-refactorings and optimizations are still sound in the gradual language.  
-Unfortunately, establishing the correctness of program transformations is 
-technically difficult---requires proofs of program equivalence---and
-often neglected in the metatheory of these languages.  
+While gradual type soundness theorems for these languages aim to show that 
+``type-based reasoning'' is preserved when moving from the fully static setting to a
+gradual one, these theorems do not imply that the correctness of type-based
+refactorings and optimizations is preserved.  Establishing correctness of
+program transformations is technically difficult---requires reasoning about
+program equivalence---and often neglected in the metatheory of gradual languages.   
 
 In this paper, we propose an \emph{axiomatic} account of program equivalence in a
 gradual cast calculus, which we formalize in a logic we call \emph{gradual type
@@ -20,7 +19,7 @@ $\beta\eta$ laws hold for a connective, then casts between that connective must
 be equivalent to the ``lazy'' cast semantics. 
 As a contrapositive, this shows that ``eager'' cast semantics violates the
 extensionality of function types.  Additionally, we show that gradual upcasts
-are pure functions and dually gradual downcasts are strict functions, an
+are pure functions and, dually, gradual downcasts are strict functions, an
 equational analogue of Wadler-Findler's blame soundness theorem.
 
 We show the consistency and applicability of our axiomatic theory by proving
diff --git a/paper/gtt.tex b/paper/gtt.tex
index eafd95c8ce8dab5f61c6c637ddab8031e2002f6d..0f18fefc1742432eca3190b88bf48817b0c5a202 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -1,15 +1,19 @@
-%% For double-blind review submission
-\documentclass[acmsmall,anonymous,review]{acmart}\settopmatter{printfolios=true}
-%% For single-blind review submission
-%\documentclass[acmlarge,review]{acmart}\settopmatter{printfolios=true}
-%% For final camera-ready submission
-%\documentclass[acmlarge]{acmart}\settopmatter{}
+%% For double-blind review submission, w/o CCS and ACM Reference (max submission space)
+\documentclass[acmsmall,review,anonymous]{acmart}\settopmatter{printfolios=true,printccs=false,printacmref=false}
+%% For double-blind review submission, w/ CCS and ACM Reference
+%\documentclass[acmsmall,review,anonymous]{acmart}\settopmatter{printfolios=true}
+%% For single-blind review submission, w/o CCS and ACM Reference (max submission space)
+%\documentclass[acmsmall,review]{acmart}\settopmatter{printfolios=true,printccs=false,printacmref=false}
+%% 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{}
 
 \newif\ifshort
 \newif\iflong
 %% Pick long or short version:
-%% \shorttrue
-\longtrue
+\shorttrue
+%%\longtrue
 
 %% Note: Authors migrating a paper from PACMPL format to traditional
 %% SIGPLAN proceedings format should change 'acmlarge' to