diff --git a/paper/gtt.tex b/paper/gtt.tex
index 88f1abe52c9cd5320bf152469d73840c01e2473b..c0f623fd79e74153a0249d73dbff754a1990e5f2 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -152,15 +152,36 @@
\begin{document}
\begin{abstract}
- We present Gradual Type Theory: an axiomatic semantics of gradual
+ We present Gradual Type Theory (GTT): an axiomatic semantics of gradual
typing.
Gradual Type Theory gives specifications to the cast semantics that
are normally part of the language definition of gradual typing.
- Since it is based on Levy's Call-by-push-value language, it supports
- embeddings of call-by-value and call-by-name gradually typed
- languages, and proves uniqueness theorems for cast/contracts in
- call-by-value and call-by-name languages with both positive and
- negative type connectives.
+ These combine the axiomatics for effectful languages provided by
+ call-by-push-value with the graduality property that says that
+ making types more precise in a gradual program only adds errors, and
+ that casts produce minimal change in program semantics.
+ The use of call-by-push-value enables us to see distinctions that
+ were not previously observed in call-by-value gradually typed
+ languages: chief among them is that while upcasts are known to
+ always terminate, \emph{downcasts} satisfy a dual property that they
+ are \emph{linear}.
+
+ Furthermore, We show that the combination of effect-aware
+ $\beta\eta$ laws and graduality is \emph{only} satsified by
+ ``wrapping'' implementations of gradual typing, and ``eager''
+ semantics violate the $\eta$ principles.
+ 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.
+
+ We give a translation of the axiomatic theory into
+ call-by-push-value with recursive types and errors.
+ We define a logical relation that models the logical notion of term
+ dynamism that is key to interpreting the dynamic gradual guarantee.
+ 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 to varying degrees of support for call-by-value and
+ call-by-name embeddings.
\end{abstract}
%% 2012 ACM Computing Classification System (CSS) concepts
@@ -463,7 +484,88 @@ Generalizing further, a stack out of an iterated function type $A_1
\subsection{Casts}
+It is not immediately obvious how to add type casts to
+call-by-push-value, but we can use previous work on call-by-value and
+call-by-name gradual typing, combined with the embeddings of CBV and
+CBN into CBPV for guidance.
+%
+In both CBV and CBN, we add a type dynamism judgment $A \ltdyn B$ and
+for every such pair, we add an upcast from $A$ to $B$: $\ucpast A B M$
+and a downcast from $B$ to $A$: $\dncast A B M$.
+%
+Then because CBV types are associated to CBPV value types and CBN
+types are associated to CBPV computation types, it seems reasonable to
+simply have a value type dynamism $A \ltdyn A'$ and computation type
+dynamism $\u B \ltdyn \u B'$ and an upcast and downcast form for each
+corresponding to the CBV and CBN casts.
+%
+A CBV terms $x : A \vdash M : A'$ is in CBPV a term $x : A \vdash M :
+\u F A'$, because in call by value values are passed as arguments,
+then effects are performed and possibly a value is returned.
+%
+A CBN term $x : \u B \vdash M : \u B'$ is in CBPV a term $x : U \u
+B\vdash M : \u B'$, because in CBN unevaluated thunks are passed as
+arguments and terms satisfy the $\eta$ laws of the computation type.
+
+\begin{figure}
+ \begin{mathpar}
+ \inferrule
+ {\Gamma \vdash V : A \and A \ltdyn A'}
+ {\Gamma \vdash \upcast {A}{A'} V : \u F A'}
+
+ \inferrule
+ {\Gamma \vdash V' : A' \and A \ltdyn A'}
+ {\Gamma \vdash \dncast {A}{A'} V' : \u F A}
+
+ \inferrule
+ {\Gamma \vdash V : U \u B \and \u B \ltdyn \u B'}
+ {\Gamma \vdash \upcast {\u B}{\u B'} V : \u B'}
+
+ \inferrule
+ {\Gamma \vdash V' : U \u B' \and \u B \ltdyn \u B'}
+ {\Gamma \vdash \dncast {\u B}{\u B'} V' : \u B'}
+ \end{mathpar}
+ \caption{Na\"ive Interpretation of Casts}
+ \label{Bad Casts}
+\end{figure}
+
+So to reproduce this in GTT, we could add casts to the language as in
+figure \ref{bad-casts}, which we call the ``na\"ive'' interpretation
+of casts.
+%
+We call it na\"ive because it is problematic for multiple reasons:
+some syntactic and some semantic.
+
+First, semantically, it is \emph{insufficient} to recover all of the
+known properties of casts in CBV: specifically that in CBV, upcasts
+always terminate without performing any effects, and in some systems
+upcasts are defined to be values.
+%
+In previous work on a logical relation for call-by-value gradual
+typing, it was possible to prove from the properties we axiomatized
+that all upcasts had this property, but this was only because we were
+working in a language whose only effects were divergence and error.
+%
+In a more
+
+The na\"ive casts are also problemantic syntactically.
+%
+The first issue is that they violate a type theoretic principle of
+\emph{modularity}:
+
+%% Counterexample
+
+%% consider a language whose only effects are error and incrementing
+%% and decrementing an integer counter.
+%%
+%% Then for closed programs with unit output, P <= P' when P ->* err
+%% or P ->* (n, ()) and P' ->* (n', ()) and n = n', where n,n' are the
+%% final counts
+
+%% Then for every type A, there are CBV coreflections (e(x) = inc; ret x | p(y) = dec; ret y)
+
+\subsection{Dynamic Type(s)}
\subsection{Embedding Call-by-Value}
@@ -483,6 +585,19 @@ interpreted as value types in call-by-push-value.
\section{Theorems in Gradual Type Theory}
+From the axiomatics of Gradual Type Theory, we can derive many
+consequences.
+
+\begin{theorem}{Casts (de)composition}
+ For any $A \ltdyn A' \ltdyn A''$ and $\u B \ltdyn \ltdyn \u B' \ltdyn \u B''$:
+ \begin{enumerate}
+ \item $x \vdash \upcast A A x \equidyn x$
+ \item $x \vdash \upcast A {A''}x \equidyn \upcast{A'}{A''}\upcast A{A'} x$
+ \item $\bullet \vdash \dncast {\u B}{\u B} \bullet \equidyn \bullet$
+ \item $\bullet \vdash \dncast {\u B}{\u B''} \bullet \equidyn \dncast{\u B}{\u B'}\dncast{\u B'}{\u B''} \bullet$
+ \end{enumerate}
+\end{theorem}
+
\section{Contract Translation to Call-by-push-value}
\subsection{Cast to Contract Translation}
@@ -499,6 +614,25 @@ interpreted as value types in call-by-push-value.
\paragraph{Casts as Galois Connections}
+\paragraph{Thunkable, Linear, Contextual Isomorphisms}
+
+Our use of complex values for upcasts and complex stacks for downcasts
+seems closely related to the use of thunkable isomorphisms and linear
+isomorphisms in polarized languages like call-by-push-value and
+sequent calculi.
+%
+Thunkability and linearity are semantic properties that say when terms
+are ``essentially'' values and stacks respectively.
+%
+Levy has proposed a notion of \emph{contextual} isomorphism of types
+that in call-by-push-value and other polarized languages correctly
+identifies that isomorphisms between value types should be thunkable
+and between computation types should be linear.
+%
+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}
As mentioned before, our gradual record types are not quite the same
@@ -554,7 +688,7 @@ downcasts to (negative) computation types
The $\eta$ law for function types, even in the appropriate form for
call-by-value is \emph{not} satisfied by so-called \emph{eager} cast
-semantics.
+semantics, which is what is produced by AGT.
%
TODO: see the cbn gtt repo.
%