diff --git a/paper/gtt.tex b/paper/gtt.tex
index 1b8c8bb2889f98985f133dbe08dce2b1f88cd09f..2bf04086ecf8288a3cbbc35fde13d192bbe55205 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -5,6 +5,12 @@
 %% For final camera-ready submission
 %\documentclass[acmlarge]{acmart}\settopmatter{}
 
+\newif\ifshort
+\newif\iflong
+%% Pick long or short version:
+%% \shorttrue
+\longtrue
+
 %% Note: Authors migrating a paper from PACMPL format to traditional
 %% SIGPLAN proceedings format should change 'acmlarge' to
 %% 'sigplan,10pt'.
@@ -238,90 +244,48 @@
 
 \begin{abstract}
   Gradually typed languages are designed to support both dynamically
-  typed and statically typed programming styles and preserve the
-  benefits of each: dynamic code can be used without conforming to the
-  syntactic type discipline, and static code provides sound reasoning
-  principles that formally justify type-based refactorings and
-  optimizations.
-  %
-  The linchpin to the design is the semantics of runtime casts that
-  ensure that the typed reasoning principles are valid by checking
-  types of dynamically typed code at runtime.
-  %
-  However, very few previous works have actually proven that the
-  runtime casts ensure correctness of type based optimizations.
+  typed and statically typed programming styles without sacrificing
+  the soundness of type-based refactorings and optimizations.
   %
-  In fact, we show that one of the most commonly proposed semantics of
-  runtime casts, the ``eager'' semantics \emph{invalidates} certain
-  type based optimization for function types that are valid in
-  statically typed languages.
+  However, establishing the correctness of program transformations is
+  technically difficult and often neglected in the metatheory of these
+  languages.
   %
-  This shows that eager semantics is ``over-eager'' to find bugs:
-  while it catches syntactic type errors earlier than the lazy
-  semantics, it disables the type-based optimizations and refactorings
-  that gradual typing is intended to enable.
+  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).
   %
-  On the other hand, we show the simpler ``lazy'' semantics of runtime
-  casts does validate the optimization.
-  %
-  This presents the question: are there other semantics that also
-  validate these optimizations?
+  Based on Levy's call-by-push-value, GTT gives an axiomatic account
+  of both call-by-value and call-by-name gradual languages.
 
-  To study this question, we define Gradual Type Theory (GTT): an
-  axiomatic semantics of gradual typing.
-  %
-  To axiomatize type based reasoning, GTT includes the $\beta, \eta$
-  equalities that are valid for effectful programs.
+  Based on our axiomatic account we prove many theorems that justify
+  optimizations and refactorings in gradually typed languages.
   %
-  To constrain the design, we also axiomatize the \emph{graduality} of
-  the system, an extensional variant of Siek-Vitousek-Cimini-Boyland's
-  gradual guarantee.
-  %
-  We base the type theory on Levy's Call-by-push-value to correctly
-  accomodate the $\eta$ principles in the presence of effects, and as
-  a consequence we model both call-by-value and call-by-name gradual
-  typing in the same system.
-
-  We use gradual type theory to show that the combination of the
-  graduality property and the $\beta, \eta$ principles \emph{uniquely
-    determines} the behavior of almost all casts of gradual typing.
-  %
-  This shows that any gradual language that supports both must be
-  equivalent to the ``wrapping'' semantics, and any system that
-  differs from it must violate graduality or extensionality (typically
-  the latter), extending a previous result for a fragment of
-  call-by-name to full call-by-name and call-by-value.
+  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.
   %
-  On the other hand the structure of the dynamic type itself, which is
-  taken for granted to be a sum in previous work, is not uniquely
-  determined by the axiomatics, and we present several designs for
-  dynamic types that to varying degrees support interoperability
-  between call-by-value and call-by-name programs.
-
-  Furthermore, taking advantage of call-by-push-value's fine-grained
-  reasoning about effects, we prove the validity of another class of
-  optimizations under very mild conditions on the dynamic type.
+  As a contrapositive, this shows that ``eager'' cast semantics
+  violates the extensionality of function types.
   %
-  Specifically, we show that all upcasts are pure (thunkable) and that
-  all downcasts are strict (linear).
+  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.
   %
-  These two properties are extremely useful for optimizations because
-  pure terms in call-by-value can be freely moved and strict terms in
-  call-by-name can justify elimination of unnecessary thunks.
+  Since GTT also axiomatizes the dynamic gradual guarantee, our
+  logical relation also establishes this central theorem of gradual
+  typing.
   %
-  We argue that these properties are the intended meaning of the blame
-  soundness theorem.
-
-  Finally, to show the consistency of our type theory, and its
-  relation to operational semantics, we give a \emph{contract
-    translation} of our gradual language into typed
-  call-by-push-value, and prove that it preserves graduality and
-  $\beta, \eta$ by developing a logical relation for
-  call-by-push-value's operational semantics.
-  %
-  Using the rich types of call-by-push-value, we vary the structure of
-  the dynamic type and produce several translations that all model the
-  axioms of GTT.
+  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.
 \end{abstract}
 
 %% 2012 ACM Computing Classification System (CSS) concepts