diff --git a/paper/ACM-Reference-Format.bst b/paper/ACM-Reference-Format.bst
index f79017ea74a6c930d7f473f08f1d0b9d1b9e90d0..f955c84baa272b4fc432a95f8d88659e5b517dce 100644
--- a/paper/ACM-Reference-Format.bst
+++ b/paper/ACM-Reference-Format.bst
@@ -2331,7 +2331,6 @@ FUNCTION { misc }
     { "\bibinfo{howpublished}{" howpublished "}" * * output }
   if$
   "" output.nonnull.dot.space
-  output.day.month.year
   calc.format.page.count output
   fin.block
   output.issue.doi.coden.isxn.lccn.url.eprint.note
@@ -2890,4 +2889,4 @@ FUNCTION { end.bib }
   writeln
 }
 
-EXECUTE {end.bib}
+EXECUTE {end.bib}
\ No newline at end of file
diff --git a/paper/abstract.tex b/paper/abstract.tex
index e876b0d08f27d74f2c580e693cc750a63c8e238d..6b549ccf9db76318fa4d104eabd501e21c2b011e 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 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/acmart.cls b/paper/acmart.cls
index 1491374305948b76ab6384341b11313b261c531b..e10b4638aa2b68e4c1bdfac271287a9c69cc2f3d 100644
--- a/paper/acmart.cls
+++ b/paper/acmart.cls
@@ -37,7 +37,7 @@
 %%   Right brace   \}     Tilde         \~}
 \NeedsTeXFormat{LaTeX2e}
 \ProvidesClass{acmart}
-[2018/01/24 v1.49 Typesetting articles for the Association for
+[2018/04/14 v1.53 Typesetting articles for the Association for
 Computing Machinery]
 \def\@classname{acmart}
 \InputIfFileExists{acmart-preload-hook.tex}{%
@@ -639,10 +639,16 @@ Computing Machinery]
     have the newtxmath package installed.  Please upgrade your
     TeX}\@ACM@newfontsfalse}
 \if@ACM@newfonts
-\RequirePackage[tt=false, type1=true]{libertine}
+\ifxetex
+  \RequirePackage[tt=false]{libertine}
+\else
+  \RequirePackage[tt=false, type1=true]{libertine}
+\fi
 \RequirePackage[varqu]{zi4}
 \RequirePackage[libertine]{newtxmath}
-\RequirePackage[T1]{fontenc}
+\ifxetex\else
+  \RequirePackage[T1]{fontenc}
+\fi
 \fi
 \let\liningnums\@undefined
 \AtEndPreamble{%
@@ -785,6 +791,7 @@ Computing Machinery]
   JERIC,%
   JETC,%
   JOCCH,%
+  PACMCGIT,%
   PACMHCI,%
   PACMPL,%
   POMACS,%
@@ -795,10 +802,12 @@ Computing Machinery]
   TALLIP,%
   TAP,%
   TCPS,%
+  TDSCI,%
   TEAC,%
   TECS,%
   THRI,%
   TIIS,%
+  TIOT,%
   TISSEC,%
   TIST,%
   TKDD,%
@@ -872,6 +881,12 @@ Computing Machinery]
 \or % JOCCH
   \def\@journalName{ACM Journal on Computing and Cultural Heritage}%
   \def\@journalNameShort{ACM J. Comput. Cult. Herit.}%
+\or % PACMCGIT
+  \def\@journalName{Proceedings of the ACM on Computer Graphics and Interactive Techniques}%
+  \def\@journalNameShort{Proc. ACM Comput. Graph. Interact. Tech.}%
+  \def\@permissionCodeOne{2577-6193}%
+  \@ACM@screentrue
+  \PackageInfo{\@classname}{Using screen mode due to \@journalCode}%
 \or % PACMHCI
   \def\@journalName{Proceedings of the ACM on Human-Computer Interaction}%
   \def\@journalNameShort{Proc. ACM Hum.-Comput. Interact.}%
@@ -913,6 +928,10 @@ Computing Machinery]
   \def\@journalName{ACM Transactions on Applied Perception}%
 \or % TCPS
   \def\@journalName{ACM Transactions on Cyber-Physical Systems}%
+\or % TDSCI
+  \def\@journalName{ACM Transactions on Data Science}%
+  \def\@journalNameShort{ACM Trans. Data Sci.}%
+  \def\@permissionCodeOne{2577-3224}%
 \or % TEAC
   \def\@journalName{ACM Transactions on Economics and Computation}%
 \or % TECS
@@ -927,6 +946,10 @@ Computing Machinery]
   \def\@journalName{ACM Transactions on Interactive Intelligent Systems}%
   \def\@journalNameShort{ACM Trans. Interact. Intell. Syst.}%
   \def\@permissionCodeOne{2160-6455}%
+\or % TIOT
+  \def\@journalName{ACM Transactions on Internet of Things}%
+  \def\@journalNameShort{ACM Trans. Internet Things}%
+  \def\@permissionCodeOne{2577-6207}%
 \or % TISSEC
   \def\@journalName{ACM Transactions on Information and System Security}%
   \def\@journalNameShort{ACM Trans. Info. Syst. Sec.}%
@@ -1154,7 +1177,7 @@ Computing Machinery]
   \g@addto@macro\@title{\footnotemark}%
   \if@ACM@anonymous
     \g@addto@macro\@titlenotes{%
-      \stepcounter{footnote}\footnotetext{#1}}%
+      \stepcounter{footnote}\footnotetext{Title note}}%
   \else
     \g@addto@macro\@titlenotes{\stepcounter{footnote}\footnotetext{#1}}%
   \fi}
@@ -1336,13 +1359,13 @@ Computing Machinery]
   \fi
   \ifnum\acm@copyrightmode=3\relax % rightsretained
    \@acmownedfalse
-   \acmPrice{}%
+   \AtBeginDocument{\acmPrice{}}%
   \fi
   \ifnum\acm@copyrightmode=4\relax % usgov
    \@printpermissiontrue
    \@printcopyrightfalse
    \@acmownedfalse
-   \acmPrice{}%
+   \AtBeginDocument{\acmPrice{}}%
   \fi
   \ifnum\acm@copyrightmode=6\relax % cagov
    \@acmownedfalse
@@ -1364,9 +1387,11 @@ Computing Machinery]
   \fi
   \ifnum\acm@copyrightmode=13\relax % iw3c2w3
    \@acmownedfalse
+   \AtBeginDocument{\acmPrice{}}%
   \fi
   \ifnum\acm@copyrightmode=14\relax % iw3c2w3g
    \@acmownedfalse
+   \AtBeginDocument{\acmPrice{}}%
   \fi}
 \def\setcopyright#1{\setkeys{ACM@}{acmcopyrightmode=#1}}
 \setcopyright{acmcopyright}
@@ -1376,7 +1401,7 @@ Computing Machinery]
   Association for Computing Machinery.
   \or % acmlicensed
   Copyright held by the owner/author(s). Publication rights licensed to
-  the Association for Computing Machinery.
+  ACM\@.
   \or % rightsretained
   Copyright held by the owner/author(s).
   \or % usgov
@@ -1388,24 +1413,24 @@ Computing Machinery]
   Association for Computing Machinery.
   \or %licensedusgovmixed
   Copyright held by the owner/author(s). Publication rights licensed to
-  the Association for Computing Machinery.
+  ACM\@.
   \or % licensedcagov
   Crown in Right of Canada. Publication rights licensed to
-  the Association for Computing Machinery.
+  ACM\@.
   \or %licensedcagovmixed
   Copyright held by the owner/author(s). Publication rights licensed to
-  the Association for Computing Machinery.
+  ACM\@.
   \or % othergov
   Association for Computing Machinery.
   \or % licensedothergov
   Copyright held by the owner/author(s). Publication rights licensed to
-  the Association for Computing Machinery.
+  ACM\@.
   \or % ic2w3www
   IW3C2 (International World Wide Web Conference Committee), published
-  under Creative Commons CC~BY~4.0 License.
+  under Creative Commons CC-BY~4.0 License.
   \or % ic2w3wwwgoogle
   IW3C2 (International World Wide Web Conference Committee), published
-  under Creative Commons CC~BY-NC-ND~4.0 License.
+  under Creative Commons CC-BY-NC-ND~4.0 License.
   \fi}
 \def\@formatdoi#1{\url{https://doi.org/#1}}
 \def\@copyrightpermission{%
@@ -1521,23 +1546,15 @@ Computing Machinery]
    only.
  \or % iw3c2w3
    This paper is published under the Creative Commons Attribution~4.0
-   International (CC~BY~4.0) license. Authors reserve their rights to
+   International (CC-BY~4.0) license. Authors reserve their rights to
    disseminate the work on their personal and corporate Web sites with
-   the appropriate attribution. In case of republication, reuse, etc.,
-   the following attribution should be used: ``Published in
-   WWW\@acmYear{} Proceedings \textcopyright{} \@copyrightyear{}
-   International World Wide Web Conference Committee, published under
-   Creative Commons~CC~BY~4.0  License.''
+   the appropriate attribution.
  \or % iw3c2w3g
    This paper is published under the Creative Commons
    Attribution-NonCommercial-NoDerivs~4.0 International
-   (CC~BY-NC-ND~4.0) license. Authors reserve their rights to
+   (CC-BY-NC-ND~4.0) license. Authors reserve their rights to
    disseminate the work on their personal and corporate Web sites with
-   the appropriate attribution. In case of republication, reuse, etc.,
-   the following attribution should be used: ``Published in
-   WWW\@acmYear{} Proceedings \textcopyright{} \@copyrightyear
-   International World Wide Web Conference Committee, published under
-   Creative Commons CC~BY-NC-ND~4.0 License.''
+   the appropriate attribution.
  \fi}
 \def\copyrightyear#1{\def\@copyrightyear{#1}}
 \copyrightyear{\@acmYear}
@@ -2216,7 +2233,7 @@ Computing Machinery]
     \fancyhead[RO]{\@headfootfont\@acmArticle\if@ACM@printfolios:\thepage\fi}%
     \fancyhead[RE]{\@headfootfont\@shortauthors}%
     \fancyhead[LO]{\ACM@linecountL\@headfootfont\shorttitle}%
-    \fancyfoot[RO,LE]{\footnotesize \@journalName, Vol. \@acmVolume, No.
+    \fancyfoot[RO,LE]{\footnotesize \@journalNameShort, Vol. \@acmVolume, No.
     \@acmNumber, Article \@acmArticle.  Publication date: \@acmPubDate.}%
   \or % acmlarge
     \fancyhead[LE]{\ACM@linecountL\@headfootfont
@@ -2224,7 +2241,7 @@ Computing Machinery]
     \fancyhead[LO]{\ACM@linecountL}%
     \fancyhead[RO]{\@headfootfont
       \shorttitle\quad\textbullet\quad\@acmArticle\if@ACM@printfolios:\thepage\fi}%
-    \fancyfoot[RO,LE]{\footnotesize \@journalName, Vol. \@acmVolume, No.
+    \fancyfoot[RO,LE]{\footnotesize \@journalNameShort, Vol. \@acmVolume, No.
     \@acmNumber, Article \@acmArticle.  Publication date: \@acmPubDate.}%
   \or % acmtog
     \fancyhead[LE]{\ACM@linecountL\@headfootfont
@@ -2233,7 +2250,7 @@ Computing Machinery]
     \fancyhead[RE]{\ACM@linecountR}%
     \fancyhead[RO]{\@headfootfont
       \shorttitle\quad\textbullet\quad\@acmArticle\if@ACM@printfolios:\thepage\fi\ACM@linecountR}%
-    \fancyfoot[RO,LE]{\footnotesize \@journalName, Vol. \@acmVolume, No.
+    \fancyfoot[RO,LE]{\footnotesize \@journalNameShort, Vol. \@acmVolume, No.
     \@acmNumber, Article \@acmArticle.  Publication date: \@acmPubDate.}%
   \else % Proceedings
     \fancyfoot[C]{\if@ACM@printfolios\footnotesize\thepage\fi}%
@@ -2302,7 +2319,7 @@ Computing Machinery]
     \fancyfoot[RO,LE]{\if@ACM@printfolios\small\thepage\fi}%
     \fancyfoot[RE,LO]{\footnotesize Manuscript submitted to ACM}%
   \or % acmsmall
-    \fancyfoot[RO,LE]{\footnotesize \@journalName, Vol. \@acmVolume, No.
+    \fancyfoot[RO,LE]{\footnotesize \@journalNameShort, Vol. \@acmVolume, No.
     \@acmNumber, Article \@acmArticle.  Publication date:
     \@acmPubDate.}%
     \fancyhead[LE]{\ACM@linecountL\@folioblob}%
@@ -2310,7 +2327,7 @@ Computing Machinery]
     \fancyhead[RO]{\@folioblob}%
     \fancyheadoffset[RO,LE]{0.6\@folio@wd}%
   \or % acmlarge
-    \fancyfoot[RO,LE]{\footnotesize \@journalName, Vol. \@acmVolume, No.
+    \fancyfoot[RO,LE]{\footnotesize \@journalNameShort, Vol. \@acmVolume, No.
     \@acmNumber, Article \@acmArticle.  Publication date:
     \@acmPubDate.}%
     \fancyhead[RO]{\@folioblob}%
@@ -2318,7 +2335,7 @@ Computing Machinery]
     \fancyhead[LO]{\ACM@linecountL}%
     \fancyheadoffset[RO,LE]{1.4\@folio@wd}%
   \or % acmtog
-    \fancyfoot[RO,LE]{\footnotesize \@journalName, Vol. \@acmVolume, No.
+    \fancyfoot[RO,LE]{\footnotesize \@journalNameShort, Vol. \@acmVolume, No.
     \@acmNumber, Article \@acmArticle.  Publication date:
     \@acmPubDate.}%
     \fancyhead[L]{\ACM@linecountL}%
@@ -2566,4 +2583,4 @@ Computing Machinery]
 \normalsize\normalfont\frenchspacing
 \endinput
 %%
-%% End of file `acmart.cls'.
+%% End of file `acmart.cls'.
\ No newline at end of file
diff --git a/paper/gtt.tex b/paper/gtt.tex
index e18c7721eac470ec7b2a0068077bdfc569deb3d0..3ab8c0c32d6a2ab620a63cbba600ff249bb5b29b 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
@@ -61,7 +65,7 @@
 %% Note: author/year citations are required for papers published as an
 %% issue of PACMPL.
 % \citestyle{acmauthoryear}   %% For author/year citations
-% 
+\setcitestyle{nosort}
 
 \title{Gradual Type Theory}
 
@@ -102,8 +106,7 @@
 \author{Amal Ahmed}
 \affiliation{
 %  \department{Department1}              %% \department is recommended
-  \institution{Northeastern University}            %% \institution is required
-  \institution{Inria Paris}            %% \institution is required
+  \institution{Northeastern University and Inria Paris}            %% \institution is required
 %  \streetaddress{Street1 Address1}
 %  \city{City1}
 %  \state{State1}
@@ -602,6 +605,7 @@ To keep the proofs high-level, we break the proof into two steps.
 %
 First, we translate the axiomatic theory of GTT into an axiomatic
 theory of CBPV extended with recursive types and an uncatchable error.
+% AA: i.e., we remove casts
 %
 Then we give an operational semantics for the extended CBPV and define
 a step-indexed biorthogonal logical relation that interprets the
@@ -609,7 +613,7 @@ ordering relation on terms as contextual error approximation, which
 underlies the definition of graduality as presented in
 \cite{newahmed2018}.
 %
-In combination these proofs give an implementation of the term
+In combination these proofs, we give an implementation of the term
 language of GTT in which $\beta, \eta$ are observational equivalences
 and the dynamic gradual guarantee is satisfied.
 
@@ -628,6 +632,8 @@ the additive units $0$ and $\top$).
 %
 We use CBPV as a metalanguage to explore the design space of the
 dynamic types.
+% AA: Need intuitive sentence about what that design space contains, what are
+% the options we're exploring, why does it matter.
 %
 We give two that support full call-by-push-value, and show that they
 have a surprising similarity to existing Scheme-like languages.
@@ -5582,9 +5588,9 @@ To do this inductively, we note that complex values and stacks are
 translated to terms that are each in some sense ``pure'' or ``total''.
 %
 Specifically, we show that complex values are translated to terms that
-satisfy a property called \emph{thunkability}, and dually, we
-translate complex stacks are translated to terms that satisfy
-\emph{linearity} (terminology from TODO: cite fuhrmann, Guillaume MM).
+satisfy a property called \emph{thunkability}, and dually, complex stacks are
+translated to terms that satisfy \emph{linearity} (terminology from TODO: cite
+fuhrmann, Guillaume MM). 
 
 A thunkable term is a term of type $M : \u F A$ that acts like $\ret
 V$.
@@ -5633,11 +5639,11 @@ $M$ is forced.
   \]
 \end{definition}
 
-The De-complexification procedure is defined as follows.
+The \emph{de-complexification} procedure is defined as follows.
 %
 We note that this translation is not the one presented in the CBPV
-monograph, but rather a more inefficient version which introduces many
-administrative redices, in CPS terminology.
+monograph, but rather a more inefficient version that, in CPS terminology,
+introduces many administrative redices.
 %
 Since we are only proving results up to observational equivalence
 anyway, the difference doesn't change any of our theorems, and makes
@@ -6238,7 +6244,7 @@ merely cosmetic.
 %
 Second, for the purposes of the step-indexed logical relation later,
 the step relation is \emph{quantitative}: we count the steps that
-unroll an recursive or corecursive type.
+unroll a recursive or corecursive type.
 %
 Finally, note that we only consider the operational semantics to be
 defined for terms of type $\cdot \vdash M : \u F (1+1)$, which we
@@ -6273,16 +6279,16 @@ consider to be the type of whole programs.
 
 We can then observe the following standard operational properties. We
 write $M \step N$ with no index when the index is irrelevant.
-\begin{lemma}[{Reduction is Deterministic}]
+\begin{lemma}[Reduction is Deterministic]
   If $M \step M_1$ and $M \step M_2$, then $M_1 = M_2$.
 \end{lemma}
 
-\begin{lemma}[{Subject Reduction}]
+\begin{lemma}[Subject Reduction]
   If $\cdot \vdash M : \u F A$ and $M \step M'$ then
   $\cdot \vdash M' : \u F A$.
 \end{lemma}
 
-\begin{lemma}[{Progress}]
+\begin{lemma}[Progress]
   If $\cdot \vdash M : \u F A$ then one of the following holds:
   \begin{enumerate}
   \item $M = \err$
@@ -6315,7 +6321,7 @@ an associated ``big-step'' semantics as follows.
   are done, otherwise by progress, $M \step M'$, so we need only
   observe that each of the cases above is preserved by $\step$.
 \end{longproof}
-\begin{definition}{Results}
+\begin{definition}[Results]
   Define the set of possible results of a boolean returning
   computation to be the set $\{ \diverge, \err, \ret \tru, \ret \fls
   \}$. We denote a result by $R$, and define a function $\result$
@@ -7112,7 +7118,7 @@ limit is a consequence.
     \omega {\u B} S_3$, then $S_1 \itylr i {\u B} S_3$
   \end{enumerate}
 \end{lemma}
-\begin{proof}
+\begin{longproof}
   Proof is by mutual lexicographic induction on the pair $(i, A)$ or
   $(i, \u B)$. All cases are straightforward uses of the inductive
   hypotheses except the shifts $U, \u F$.
@@ -7139,7 +7145,7 @@ limit is a consequence.
     \[ S_1[\ret V_1] \ix\apreorder j \result(S_2[\ret V_2]) \]
     which holds by assumption.
   \end{enumerate}
-\end{proof}
+\end{longproof}
 
 \begin{lemma}{Logical Relation is Quantitatively Transitive (Open Terms)}
   \begin{enumerate}
@@ -7156,7 +7162,7 @@ limit is a consequence.
     $\Gamma\pipe \bullet : \u B \vDash S_1 \ilr i S_3 \in \u B'$.
   \end{enumerate}
 \end{lemma}
-\begin{proof}
+\begin{longproof}
   \begin{enumerate}
   \item By induction on the length of the context, follows from closed value case.
   \item Assume $\gamma_1 \itylr i \Gamma \gamma_2$ and $S_1 \itylr i {\u B} S_2$.
@@ -7175,7 +7181,7 @@ limit is a consequence.
     \omega A V_3[\gamma_2]$ so the result holds by the closed case.
   \item Stack case is essentially the same as the value case.
   \end{enumerate}
-\end{proof}
+\end{longproof}
 
 \begin{corollary}{Logical Relation is Transitive in the Limit}
   \begin{enumerate}
@@ -7482,7 +7488,7 @@ following theorem that says our logical relation is a model of CBPV.
   following hold:
   \begin{mathpar}
     \Gamma \pipe \Delta \vDash E \ix\precltdyn i E' \in \u B\and
-    \Gamma \pipe \Delta \vDash E' \ix\ltdynsucc i E \in \u B
+    \Gamma \pipe \Delta \vDash E' \ix{\mathrel{\preceq\gtdyn}} i E \in \u B
   \end{mathpar}
 \end{lemma}
 
@@ -7534,36 +7540,59 @@ However, a slightly strange property is that in Levy's paper, all
 contextual morphisms are isomorphisms so we are not sure how this
 relates to our system.
 
-\paragraph{Abstracting Gradual Typing}
+\paragraph{Gradual Typing Frameworks}
 
-As mentioned before, our gradual record types are not quite the same
-as those presented in \cite{AGT} for two reasons.
+Our approach to systemactically producing a gradual type theory from a
+type theory is similar in spirit to ``frameworks'' for gradual typing,
+specifically AGT \cite{AGT} and the Gradualizer \cite{gradualizer}.
 %
-First, the unkown fields of the record may have arbitrary effects such
-as printing or divergence when invoked, whereas in AGT they can only
-error.
+Both approaches systematically produce a gradual language from a
+statically typed language, and the Gradualizer in particular has been
+implemented as an automated tool.
 %
-However, in principle it is not difficult to make a similar type by
-adapting CBPV to incorporate some basic effect distinctions.
+Furthermore, both approaches produce a surface language with a type
+system, whereas we consider only the inequational theory of
+intrinsically typed terms of a cast calculus.
 %
-For instance instead of having a single sort of computation types,
-there could be \emph{erroring computation types}, \emph{diverging
-  computation types}, etc.
+The major point of departure for this work is that both AGT and the
+Gradualizer are based on the \emph{operational semantics} of the
+statically typed language, whereas our approach is to ``gradualize''
+the axiomatic semantics of the typed language.
 %
-Then the gradual row would be accurately modeled as $\Pi_{i \in F}
-F_{\err}\dynv$ where $F_{\err}$ is an error computation type that
-cannot print or diverge.
+This means our approach accomplishes something quite different: their
+frameworks produce specific implementations, whereas our approach is
+about finding commonalities across different implementations.
 
-Second, a value of our record type might have \emph{infinitely many}
-fields that are not error, whereas in AGT they only have records with
-finite support.
+Furthermore, while both of their approaches prove various gradual
+typing correctness theorems by construction (gradual type safety,
+conservativity, gradual guarantee), neither considers the program
+equivalences that we argued are the raison d'\^etre of gradual typing
+in the first place.
+%
+In fact, the systems both \emph{fail} to preserve these equivalences.
+%
+First, AGT reproduces the ``eager'' semantics of function casts,
+breaking the $\eta$ equality of functions.
+%
+Gradualizer on the other hand produces the ``lazy'' semantics and thus
+should validate the $\eta$ equality, though this does not seem to be a
+central component of the language: a different version of gradualizer
+could produce the eager semantics and satisfy all of their criteria.
+%
+Both systems on the other hand, fail to preserve the program
+equivalences of parametric polymorphism, and in addition fail to meet
+gradual typing criteria for stateful references.
 %
-However this is a standard problem when using the ``infinitely wide
-syntax'' we used and is addressed in (TODO: call-by-push-value? Noam's
-omega paper?)
+While we have not considered these features, we have reason to believe
+that our approach will be more successful: specifically, the
+``reason'' that all of these occur is that they are not safety
+properties of the operational semantics, and the operational semantics
+is the only input to these frameworks.
 %
-It should be the case that the terms in AGT are the subset of ours
-that are definable using the upcasts and downcasts in that language.
+Therefore, from our perspective the right approach to gradualizing
+polymorphism and state is to start with the rich \emph{relational
+  logics} for program equivalence that have been developed for these
+features (TODO: citessss).
 
 \paragraph{Blame and Upcasts and Downcasts}