diff --git a/paper/gtt.tex b/paper/gtt.tex
index e6d7de59c7fdc18893cbbc158250dd80b1c691bd..fdc75d651b0629ab523988d619a4e6a406865843 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -198,6 +198,7 @@
\newcommand{\too}{\kw{to}}
\newcommand{\case}{\kw{case}}
\newcommand{\kw}[1]{\texttt{#1}\,\,}
+\newcommand{\absurd}{\kw{absurd}}
\newcommand{\caseofXthenYelseZ}[3]{\case #1 \{ #2 \pipe #3 \}}
\newcommand{\pmpairWtoXYinZ}[4]{\kw{split} #1\,\kw{to} (#2,#3). #4}
\newcommand{\pmmuXtoYinZ}[3]{\kw{unroll} #1 \,\kw{to} \roll #2. #3}
@@ -207,6 +208,13 @@
\newcommand{\abort}{\kw {abort}}
\newcommand{\with}{\mathbin{\&}}
+\newcommand{\bnfalt}{\mathrel{\bf \,\mid\,}}
+\newcommand{\alt}{\bnfalt}
+\newcommand{\bnfdef}{\mathrel{\bf ::=}}
+\newcommand{\bnfadd}{\mathrel{\bf +::=}}
+\newcommand{\bnfsub}{\mathrel{\bf -::=}}
+
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{document}
@@ -616,8 +624,6 @@ 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
@@ -706,6 +712,35 @@ TODO: do we actually know what would go wrong in that case?
%% Then for every type A, there are CBV coreflections (e(x) = inc; ret x | p(y) = dec; ret y)
+\begin{figure}
+ \begin{mathpar}
+ \inferrule
+ {\Gamma \vdash V : A \and A \ltdyn A'}
+ {\Gamma \vdash \upcast A {A'} V : A'}
+
+ \inferrule
+ {}
+ {x : A \vdash x \ltdyn \upcast A {A'} x : A \ltdyn A'}
+
+ \inferrule
+ {}
+ {x \ltdyn x' : A \ltdyn A' \vdash \upcast A {A'} x \ltdyn x' : A'}
+
+ \inferrule
+ {\Gamma\pipe \Delta \vdash M : \u B' \and \u B \ltdyn \u B'}
+ {\Gamma\pipe \Delta \vdash \dncast{\u B}{\u B'} M : \u B}
+
+ \inferrule
+ {}
+ {\bullet : \u B' \vdash \dncast{\u B}{\u B'} \bullet \ltdyn \bullet : \u B \ltdyn \u B'}
+
+ \inferrule
+ {}
+ {\bullet \ltdyn \bullet : \u B \ltdyn \u B' \vdash \bullet \ltdyn \dncast{\u B}{\u B'} \bullet : \u B}
+ \end{mathpar}
+ \caption{Casts in GTT}
+\end{figure}
+
\subsection{Dynamic Type(s)}
\subsection{Embedding Call-by-Value}
@@ -723,6 +758,57 @@ The key feature of call-by-value is that all of its types are
interpreted as value types in call-by-push-value.
%
+\begin{figure}
+ \begin{mathpar}
+ \begin{array}{lrcl}
+ \text{Types} & A & \bnfdef & 1 \alt (A + A) \alt (A \times A) \alt (A_1,\ldots,A_n) \to A\\
+ \text{Values} & V & \bnfdef & \upcast{A}{A'}V \alt () \alt \inl V \alt \inr V \alt (V,V) \alt \lambda (x_1:A_1,\ldots,x_n:A_n). M\\
+ \text{Terms} & M & \bnfdef & \err V \alt \alt \dncast{A}{A'}V \alt \caseofXthenYelseZ V {\inl x_1. M_1}{\inr x_2. M_2} \alt \pmpairWtoXYinZ V x y M \alt V(V_1,\ldots,V_n) \alt \bindXtoYinZ M x M \alt \letXbeYinZ V x M
+ \end{array}
+ \end{mathpar}
+
+ \begin{mathpar}
+ \inferrule
+ {\Gamma \vdash V : A \and A \ltdyn A'}
+ {\Gamma \vdash \upcast A {A'} V : A'}
+
+ \inferrule
+ {\Gamma \vdash V : A' \and A \ltdyn A'}
+ {\Gamma \vdash \dncast A {A'} V : A}
+
+ \inferrule
+ {}
+ {x : A' \vdash \dncast A A' x \ltdyn x : A \ltdyn A'}
+
+ \inferrule
+ {}
+ {x \ltdyn x' : A \ltdyn A' \vdash x \ltdyn \dncast A {A'} x : A}
+ \end{mathpar}
+ \caption{CBV GTT}
+\end{figure}
+
+\begin{figure}
+ \begin{mathpar}
+ \inferrule
+ {A \ltdyn A' \and B \ltdyn B'}
+ {f : A \to B \vdash \dncast{A\to B}{A' \to B'} f \equidyn \lambda (x:A). \bindXtoYinZ {f(\upcast{A}{A'}x)} y \dncast{B}{B'} y}
+
+ \inferrule
+ {
+ f \ltdyn \lambda (x:A). \bindXtoYinZ {f(x)} y y
+ \and
+ \inferrule
+ {\inferrule
+ {\inferrule{f \ltdyn f'\and x \ltdyn \upcast{A}{A'}x}{{f(x)} \ltdyn f'(\upcast{A}{A'}x)} \and {y \ltdyn y' \vdash y \ltdyn \dncast{B}{B'} y}}
+ {x \ltdyn x : A \vdash \bindXtoYinZ {f(x)} y y \ltdyn \bindXtoYinZ {f'(\upcast{A}{A'}x)} y' \dncast{B}{B'} y}
+ }
+ {\lambda (x:A). \bindXtoYinZ {f(x)} y y \ltdyn \lambda (x:A). \bindXtoYinZ {f'(\upcast{A}{A'}x)} y' \dncast{B}{B'} y}
+ }
+ {f \ltdyn f' : A \to B \ltdyn A' \to B'
+ \vdash f \ltdyn \lambda (x:A). \bindXtoYinZ {f'(\upcast{A}{A'}x)} y' \dncast{B}{B'} y'}
+ \end{mathpar}
+ \caption{Uniqueness Principle for CBV Functions}
+\end{figure}
\section{Theorems in Gradual Type Theory}
@@ -743,7 +829,23 @@ Gradual Type Theory.
\subsection{Upcasts are Thunkable, Downcasts are Linear, a posteriori}
-While we have shown
+\begin{theorem}{Upcasts are (Complex) Values, Downcasts are (Complex) Stacks}
+ If the tagging upcasts are complex values and untagging downcasts
+ are stacks, then all upcasts are complex values and all downcasts
+ are complex stacks.
+\end{theorem}
+\begin{proof}
+
+\end{proof}
+
+\subsection{Retract Axiom}
+
+In the call-by-name version of GTT (\cite{GTT}), there was an explicit
+axiom that states that every pair of upcasts and downcasts forms a
+section-retraction pair: i.e., that the downcast applied to the upcast
+is the identity.
+%
+
\subsection{Uniqueness Principles for Casts}
@@ -754,11 +856,95 @@ principles of each type, given in figure TODO ref.
\begin{figure}
\begin{mathpar}
- TODO
+ \upcast{0}{A}V \equidyn \absurd V\\
+ \dncast{\u F 0}{\u F A} \equidyn \err\\
+
+ \dncast{1}{\u B} \equidyn \{\}\\
+ \upcast{U 1}{U \u B} \equidyn \thunk \err\\
\end{mathpar}
\caption{Uniqueness Principles for Casts}
\end{figure}
+To prove these uniqueness theorems, we use the fact that the
+specification of upcasts and downcasts by their right and left
+$\ltdyn$ rules defines them \emph{uniquely} up to $\equidyn$.
+%
+In category-theoretic terms this says that the upcasts and downcasts
+have a \emph{universal property}, and so we can show that something
+else is equivalent to the upcast or downcast by showing that it has
+the \emph{same} property.
+%
+
+\begin{lemma}{Specification for Casts is a Universal Property}
+ If $A \ltdyn A'$ and $x : A \vdash V_u[x] : A'$ is a value such that
+ the following judgments are provable:
+ \begin{mathpar}
+ \inferrule
+ {}
+ {x : A \ltdyn x' : A' \vdash V_u[x] \ltdyn x' : A'}
+
+ \inferrule
+ {}
+ {x_2 : A \ltdyn x : A \vdash x_2 \ltdyn V_u[x] : A \ltdyn A'}
+ \end{mathpar}
+
+ then we can prove $x : A \vdash V_u[x] \equidyn x : A$.
+
+ Similarly, if $\u B \ltdyn \u B'$ and $\bullet : \u B' \vdash S_d :
+ \u B$ is a stack such that the following are provable:
+ \begin{mathpar}
+ \inferrule
+ {}
+ {\bullet \ltdyn \bullet : \u B' \vdash S_d \ltdyn \bullet : \u B \ltdyn \u B'}
+
+ \inferrule
+ {}
+ {\bullet \ltdyn \bullet : \u B \ltdyn \u B' \vdash \bullet \ltdyn S_d : \u B}
+ \end{mathpar}
+ then we can prove $\bullet : \u B' \vdash S_d \equidyn \dncast{\u B}{\u B'}\bullet : \u B$
+\end{lemma}
+\begin{proof}
+ \begin{mathpar}
+ \inferrule*[right=substitution]
+ {x_1 \ltdyn x_2 \vdash x_1 \ltdyn \upcast{A}{A'}x_2 : A \ltdyn A' \and x_1 \ltdyn x_2' : A \ltdyn A' \vdash V_u[x_1] \ltdyn x_2' : A'}
+ {x_1 : A \ltdyn x_2 : A \vdash V_u[x_1] \ltdyn \upcast{A}{A'} x_2 : A'}
+ \end{mathpar}
+ The other direction is essentially the same, but swapping $V_u$ and
+ the upcast.
+\end{proof}
+
+The other key ingredient to the uniqueness theorems is the
+\emph{$\eta$ principle} and \emph{congruence rules} for each type.
+%
+The reason for this is that to show that an implementation of a cast
+$x : A \vdash V_u : A'$ is correct, we have to show that it is less
+than and greater than \emph{variables}: $x : A \ltdyn V_u[x]$ and $x
+\ltdyn x' \vdash V_u[x] \ltdyn x'$.
+%
+Since we know nothing about a variable except it's type, the only way
+to proceed is to $\eta$ expand it.
+%
+The uniqueness principles for casts arise when the two sides of the
+cast have the \emph{same} top-level connective, and thus the
+\emph{same} $\eta$ principle, so we $\eta$ expand both the lower
+bounding and upper bounding variable, and the cast itself is a kind of
+$\eta$-expansion \emph{up to cast at smaller type}.
+
+% TODO: can we take advantage of duality???
+%% With the large number of connectives comes a large number of proofs.
+%% %
+%% For each connective, we need four proofs: left and right rules for the
+%% upcast and left and right rules for the downcast.
+%% %
+%% However, we can take advantage of the duality between upcasts and
+%% downcasts and the duality between $\ltdyn$ and $\gtdyn$ to save some
+%% effort, so that if we constrain our proof, we can mechanically turn a
+%% single case, say the left rule for upcast into proofs of the other 3
+%% cases.
+%% %
+%% In order for this duality to be \emph{perfect}, we use the version of
+%% casts that are \emph{not} assumed to be
+
\section{Contract Translation to Call-by-push-value}
To show the soundness of our model, and demonstrate its relationship