diff --git a/paper/abstract.tex b/paper/abstract.tex
index 7d09bcf8b969e002909cdd819b2edc5c35b57d6b..bffa9dfec999b086955564bce8738ad52ac88bad 100644
--- a/paper/abstract.tex
+++ b/paper/abstract.tex
@@ -7,7 +7,9 @@ not imply that correctness of type-based refactorings and optimizations
 is preserved.  Establishing correctness of program transformations is
 technically difficult, because it requires reasoning about program
 equivalence, and is often neglected in the metatheory of gradual
-languages.  In this paper, we propose an \emph{axiomatic} account of
+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
diff --git a/paper/gtt.tex b/paper/gtt.tex
index b0ce0e6d418190ad4a2bf386f03725dd1a8c71c8..477d89be0001a5932c3e490f3845d52d70a79297 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -562,15 +562,14 @@ The cast reductions that we show satisfy all of these constraints are
 those given by the ``lazy cast semantics'' (in the terminology of
 \cite{siek+09designspace})
 %
-For instance, a transient semantics, where only the first level
-connectives are checked, violates $\eta$ (for example, in the context
-${x : A_1 \times (A_2 \times A_3)}$ $\letXbeYinZ x {(x_1,(x_2,x_3))} 0$
-is not equivalent to $0$; this is provable in GTT as a consequence of
-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$ 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 $.
+For instance, a transient semantics, where only the first level connectives are
+checked, violates $\eta$ (for example, in the context
+${x : A_1 \times (A_2 \times A_3)}$ $\letXbeYinZ x {(x_1,(x_2,x_3))} 0$ is not
+equivalent to $0$; this is provable in GTT as a consequence of 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$ 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 provide a concrete example in the appendix.
 %
 Thus, we argue that ``eager'' cast semantics is in fact overly eager: in
@@ -585,17 +584,17 @@ states that for any $\lambda$-term $M \equiv \lambda x. M x$, is
 restricted in a typed language to only hold for terms of function type $M
 : A \to B$.
 %
-While this famously ``fails'' to hold in call-by-value languages in the
-presence of effects (if $M$ is a program that prints \texttt{"hello"}
-before returning a function then $M$ will print \emph{now} whereas
-$\lambda x. M x$ will only print when given an argument), this is also
-not an obstacle, because the $\eta$ law is valid in some call-by-value
-languages (e.g. SML) if we have a ``value restriction'' $V \equiv
-\lambda x. V x$ or otherwise restrict to non-effectful programs.
+While this famously ``fails'' to hold in call-by-value languages in the presence
+of effects (if $M$ is a program that prints \texttt{"hello"} before returning a
+function then $M$ will print \emph{now} whereas $\lambda x. M x$ will only print
+when given an argument), this is also not an obstacle, because the $\eta$ law is
+valid in some call-by-value languages (e.g. SML) if we have a ``value
+restriction'' $V \equiv \lambda x. V x$ or otherwise restrict to non-effectful
+programs.
 %
-This illustrates that $\eta$/extensionality rules must be stated for
-each type connective, and be sensitive to the effects/evaluation order
-of the terms involved.
+This illustrates that $\eta$/extensionality rules must be stated for each type
+connective, and be sensitive to the effects/evaluation order of the terms
+involved.
 %
 For instance, the $\eta$ principle for the boolean type $\texttt{Bool}$
 in call-by-value is that for any term $M$ with a free variable $x :
@@ -607,10 +606,10 @@ If we have an \texttt{if} form that is strongly typed (i.e., errors on
 non-booleans) then this tells us that it is \emph{safe} to run an if
 statement on any input of boolean type.
 %
-In addition, even if our \texttt{if} statement does some kind of
-coercion, this tells us that the term $M$ only cares about whether $x$ is
-``truthy'' or ``falsy'' and so a client of this code is free to change
-e.g. one truthy value to a different one without changing the behavior.
+In addition, even if our \texttt{if} statement does some kind of coercion, this
+tells us that the term $M$ only cares about whether $x$ is ``truthy'' or
+``falsy'' and so a client of this code is free to change e.g. one truthy value
+to a different one without changing the behavior.
 %
 This $\eta$ principle justifies a number of program optimizations,
 such as dead-code and common subexpression elimination, and 
@@ -637,22 +636,20 @@ domain-theoretic but not operational models of the axioms.
 
 In this paper, we develop an axiomatic gradual type theory for a unified
 language that includes \emph{both} call-by-value/eager types and
-call-by-name/lazy types (Sections~\ref{sec:gtt},
-\ref{sec:theorems-in-gtt}), and show that it is sound for contextual
-equivalence via a logical relations model (Sections~\ref{sec:contract},
-\ref{sec:complex}, \ref{sec:operational}).  Because the $\eta$
-principles for types play a key role in our approach, it is necessary to
-work in a setting where we can have $\eta$ principles for both eager and
-lazy types.  One such setting is Levy's
-Call-by-Push-Value~\citep{levy03cbpvbook} (CBPV), which fully and
-faithfully embeds both call-by-value and call-by-name evaluation, with
-both eager and lazy datatypes,\footnote{The distinction between ``lazy''
-  vs ``eager'' casts above is different than lazy vs. eager datatypes.}
-and underlies much recent work on reasoning about effectful
-programs~\cite{bauerpretnar13eff,lindley+17frank}.  This allows us to prove
-results about existing call-by-value gradually typed languages, and also
-suggests a design for call-by-name and even full call-by-push-value
-gradually typed languages.
+call-by-name/lazy types (Sections~\ref{sec:gtt}, \ref{sec:theorems-in-gtt}), and
+show that it is sound for contextual equivalence via a logical relations model
+(Sections~\ref{sec:contract}, \ref{sec:complex}, \ref{sec:operational}).
+Because the $\eta$ principles for types play a key role in our approach, it is
+necessary to work in a setting where we can have $\eta$ principles for both
+eager and lazy types.  One such setting is Levy's
+Call-by-Push-Value~\citep{levy03cbpvbook} (CBPV), which fully and faithfully
+embeds both call-by-value and call-by-name evaluation, with both eager and lazy
+datatypes,\footnote{The distinction between ``lazy'' vs ``eager'' casts above is
+  different than lazy vs. eager datatypes.}  and underlies much recent work on
+reasoning about effectful programs~\cite{bauerpretnar13eff,lindley+17frank}.
+This allows us to prove results about existing call-by-value gradually typed
+languages, and also suggests a design for call-by-name and even full
+call-by-push-value gradually typed languages.
 
 We show that the axiomatic gradual type theory approach of \cite{newlicata2018-fscd}
 applies to call-by-(push)-value.  In this approach, general casts are
@@ -671,32 +668,29 @@ stipulated in advance.  The specification defines the
 casts ``uniquely up to equivalence'', which means that any two
 implementations satisfying it are behaviorly equivalent.
 
-One of our main contributions (Section~\ref{sec:gtt}) is to generalize
-this axiomatic approach to call-by-push-value, where there are
-both eager/value types and lazy/computation types. This is both a
-subtler question than it might at first seem, and has a surprisingly
-nice answer: we find that upcasts are naturally associated with
-eager/value types and downcasts with lazy/computation types, and that
-the modalities relating values and computations induce the downcasts for
-eager/value types and upcasts for lazy/computation types.  Moreover,
-this analysis articulates an important behavioral property of casts that
-was proved operationally for call-by-value in \cite{newahmed18} but missed for
-call-by-name in \cite{newlicata2018-fscd}: upcasts for eager types and downcasts for
-lazy types are both ``pure'' in a suitable sense, which enables more
-refactorings and program optimizations.  In particular, we show that
-these casts can be taken to be (and are essentially forced to be)
-``complex values'' and ``complex stacks'' (respectively) in
-call-by-push-value, which corresponds to a behavioral property of
-\emph{thunkability} and \emph{linearity}~\cite{munchmaccagnoni14nonassociative}.  We argue in
-Section~\ref{sec:related} that this property is related to blame
-soundness.  Our gradual type theory naturally has two dynamic types, a
-dynamic eager/value type and a dynamic lazy/computation type, where the
-former can be thought of as a sum of all possible values, and the latter
-as a product of all possible behaviors.  These axioms imply that,
-for a variety of eager/value and lazy/computation types, the ``lazy
-contract'' semantics of casts is the unique implementation
-satisfying $\beta,\eta$ and graduality
-(Section~\ref{sec:theorems-in-gtt}).
+One of our main contributions (Section~\ref{sec:gtt}) is to generalize this
+axiomatic approach to call-by-push-value, where there are both eager/value types
+and lazy/computation types. This is both a subtler question than it might at
+first seem, and has a surprisingly nice answer: we find that upcasts are
+naturally associated with eager/value types and downcasts with lazy/computation
+types, and that the modalities relating values and computations induce the
+downcasts for eager/value types and upcasts for lazy/computation types.
+Moreover, this analysis articulates an important behavioral property of casts
+that was proved operationally for call-by-value in \cite{newahmed18} but missed
+for call-by-name in \cite{newlicata2018-fscd}: upcasts for eager types and
+downcasts for lazy types are both ``pure'' in a suitable sense, which enables
+more refactorings and program optimizations.  In particular, we show that these
+casts can be taken to be (and are essentially forced to be) ``complex values''
+and ``complex stacks'' (respectively) in call-by-push-value, which corresponds
+to a behavioral property of \emph{thunkability} and
+\emph{linearity}~\cite{munchmaccagnoni14nonassociative}.  We argue in
+Section~\ref{sec:related} that this property is related to blame soundness.  Our
+gradual type theory naturally has two dynamic types, a dynamic eager/value type
+and a dynamic lazy/computation type, where the former can be thought of as a sum
+of all possible values, and the latter as a product of all possible behaviors.
+These axioms imply that, for a variety of eager/value and lazy/computation
+types, the ``lazy contract'' semantics of casts is the unique implementation
+satisfying $\beta,\eta$ and graduality (Section~\ref{sec:theorems-in-gtt}).
 
 %% Morever, working in a setting with mixed eager/value and
 %% lazy/computation types often leads to more insight into each than
@@ -7616,6 +7610,7 @@ consider to be the type of whole programs.
 
 \begin{figure}
 \begin{small}
+\begin{minipage}[t]{0.65\textwidth}
 \[
   \begin{array}{rcl}
     S[\err] &\stepzero& \err\\
@@ -7632,15 +7627,22 @@ consider to be the type of whole programs.
     S[\unroll \rollty{\u B} M] &\stepone & S[M]\\
 \end{array}
 \]
+\end{minipage}
+\begin{minipage}[t]{0.27\textwidth}
+\vspace{3em}
 \begin{mathpar}
+
     \inferrule
     {}
     {M \bigstepsin 0 M}
 
+\vspace{1.3em}
+
     \inferrule
     {M_1 \stepsin{i} M_2 \and M_2 \bigstepsin j M_3}
     {M_1 \bigstepsin {i+j} M_3}
   \end{mathpar}
+\end{minipage}
   \end{small}
   \caption{CBPV Operational Semantics}
   \label{fig:cbpv-operational-semantics}
diff --git a/paper/max.bib b/paper/max.bib
index 00ef0b307b6a630510c4ad730843fb6082c59e3d..4605248f28cc7ce98e5a372eeea04efe4ed32055 100644
--- a/paper/max.bib
+++ b/paper/max.bib
@@ -115,7 +115,7 @@
 @STRING{icfp15 =    icfp # ", Vancouver, British Columbia, Canada" }
 @STRING{icfp16 =    icfp # ", Nara, Japan" }
 @STRING{icfp17 =    icfp # ", Oxford, United Kingdom" }
-@STRING{icfp18 =    icfp # ", Saint Louis, Missouri" }
+@STRING{icfp18 =    icfp # ", St. Louis, Missouri" }
 
 % ----
 @STRING{oopsla =    "{ACM} {S}ymposium on {O}bject {O}riented {P}rogramming: