diff --git a/paper/gtt.tex b/paper/gtt.tex
index b7d195f0b445b801b65ebdb47b602c1812c7a919..77409cb0c9d44a48e7feb8bfe50f7561ae6d1f27 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -4508,7 +4508,7 @@ The following lemma shows this forms a computation ep pair:
 
 From this, we see that the easiest way to construct an interpretation
 of the dynamic computation type is to make it a lazy product of all
-the ground types $\u G$: $\dynv \cong \With_{\u G} \u G$.
+the ground types $\u G$: $\dyns \cong \With_{\u G} \u G$.
 
 Using recursive types, we can easily make this a definition of the
 interpretations:
@@ -9335,6 +9335,58 @@ casts~\cite{siekwadler10zigzag}, are equivalent to the lazy contract
 semantics, they should also be models of GTT, and if so we could use GTT
 to reason about program transformations and optimizations in them.
 
+We plan to use this core calculus as a target language for multiple
+high level gradually typed languages, with the high-level languages
+inheriting proofs of graduality and appropriate forms of $\eta$
+equivalence.
+%
+We have focused on the application to call-by-value source languages
+because almost all work on gradually typed languages has taken place
+in a call-by-value setting.
+
+While call-by-value evaluation is a fairly consistent notion,
+non-eager evaluation comes in many flavors.
+%
+Not only is there the distinction between call-by-name and
+call-by-need, but in practice lazy languages like Haskell contain
+operators like \texttt{seq} in Haskell that force strict evaluation
+and invalidate the call-by-name $\eta$ principle.
+%
+Call-by-push-value has been shown to embed call-by-name evaluation
+\emph{without} the presence of the \texttt{seq} operator or any
+analogous operation where the function type is modeled as $UB \to B'$.
+%
+To apply our framework to call-by-name languages that support
+\texttt{seq}, we would need to first provide an embedding into
+call-by-push-value that supports this operation.
+%
+This seems feasible, for instance a function $\texttt{Number} \to
+\texttt{String}$ would be interpreted as $UFU(UF\texttt{Number}\to
+\texttt{String})$, where the extra $UF$ models the fact that we can
+force the function to a value without necessarily calling it by using
+\texttt{seq}.
+%
+In this sense, Haskell's behavior is similar to call-by-value in that
+it satisfies a modified $\eta$ principle for functions: $x =
+\texttt{seq} x (\lambda y. x y)$ where $x$ is a variable.
+%
+If this embedding is correct, then just as with call-by-value, GTT
+provides a semantics of casts that satisfies graduality and validates
+this $\eta$ principle.
+%
+In future work, we plan to do a more thorough analysis of the
+resulting semantics and compare to previous proposals for lazy
+contract semantics (TODO cite).
+%
+Finally note that once we have introduced the extra thunks to model
+\texttt{seq}, if the only effects used are idempotent then the
+difference between call-by-name and call-by-need is only relevant for
+performance reasons.
+%
+Therefore the resulting semantics we produce should also be relevant
+for call-by-need evaluation.
+
+
 Some recent work \cite{greenmanfelleisen:2018} gives a spectrum of
 differing syntactic type soundness theorems for different semantics of
 gradual typing.