diff --git a/paper/abstract.tex b/paper/abstract.tex
new file mode 100644
index 0000000000000000000000000000000000000000..19f1fb96a2d80175a58a0a336f750fc40980d5ed
--- /dev/null
+++ b/paper/abstract.tex
@@ -0,0 +1,34 @@
+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 and often neglected in the metatheory of these 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
+theory} (GTT). Based on Levy's call-by-push-value, GTT gives an axiomatic account
+of both call-by-value and call-by-name gradual languages.
+
+Based on our axiomatic account we prove many theorems that justify optimizations
+and refactorings in gradually typed languages. For example, we show what we call
+\emph{uniqueness principles} for gradual type connectives that show that if the
+$\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
+equational analogue of Wadler-Findler's blame soundness theorem.
+
+We show the consistency and applicability of our axiomatic theory by proving
+that a contract-based implementation using the lazy cast semantics gives a model
+of our type theory where equivalence in GTT implies contextual equivalence of
+the programs.  Since GTT also axiomatizes the dynamic gradual guarantee, our
+logical relation also establishes this central theorem of gradual typing.
+Finally, we define \emph{multiple} contract-based implementations by varying the
+structure of the dynamic types, giving a family of implementations that validate
+type-based optimization and the gradual guarantee.
+
+% AA: above "logical relation" comes out of the blue
\ No newline at end of file
diff --git a/paper/gtt.tex b/paper/gtt.tex
index 78180ee76e6f2cea4db794b21ad528f3ac625be6..b44876c6955c8229a68ea9a3f46faa4c75978bb8 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -271,49 +271,7 @@
 \begin{document}
 
 \begin{abstract}
-  Gradually typed languages are designed to support both dynamically
-  typed and statically typed programming styles without sacrificing
-  the soundness of type-based refactorings and optimizations.
-  %
-  However, establishing the correctness of program transformations is
-  technically difficult and often neglected in the metatheory of these
-  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 theory} (GTT).
-  %
-  Based on Levy's call-by-push-value, GTT gives an axiomatic account
-  of both call-by-value and call-by-name gradual languages.
-
-  Based on our axiomatic account we prove many theorems that justify
-  optimizations and refactorings in gradually typed languages.
-  %
-  For example, we show what we call \emph{uniqueness principles} for
-  gradual type connectives that show that if the $\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 equational
-  analogue of Wadler-Findler's blame soundness theorem.
-
-  We show the consistency and applicability of our axiomatic
-  theory by proving that a contract-based implementation using the
-  lazy cast semantics gives a model of our type theory where
-  equivalence in GTT implies contextual equivalence of the programs.
-  %
-  Since GTT also axiomatizes the dynamic gradual guarantee, our
-  logical relation also establishes this central theorem of gradual
-  typing.
-  %
-  Finally, we define \emph{multiple} contract-based implementations by
-  varying the structure of the dynamic types, giving a family of
-  implementations that validate type-based optimization and the
-  gradual guarantee.
+\input{abstract}
 \end{abstract}
 
 %% 2012 ACM Computing Classification System (CSS) concepts
@@ -411,8 +369,9 @@ to the user: we have all of the syntactic discipline but none of the
 semantic rewards.
 %
 In a gradually typed language, type annotations mean that we are relieved of the
-burden of reasoning about incorrect inputs---as in a static language---as long
-as we are willing to accept that the program as a whole may crash. 
+burden of reasoning about incorrect inputs in the statically typed
+fragment of the language, as long as we are willing to accept that the program
+as a whole may crash.  
 %
 The upside is that in \emph{effectful} languages this is hardly
 different from full static typing: we already accept the possibility that