some headline theorems

paper/gtt.tex

@@ -760,9 +760,31 @@ While contracts are typically implemented in a dynamically typed
 language, our target is typed, meaning we retain the type information
 that might be used in later stages of compilation.
 %
-We could always erase the types of our typed language (cbpv's
-operational semantics is perfectly sensible on untyped terms) and get
-a more typical contract translation.
+We could erase the types of our typed language and translate to some
+dynamically typed version of cbpv to get a more typical contract
+translation, but we leave this to future work.
+
+In particular the aim of this section is to establish the following
+theorems:
+
+\begin{theorem}{Consistency of GTT}
+  There exists a judgment $\Gamma_1 \ltdyn \Gamma_2 \vdash M_1 \ltdyn
+  M_2 : B_1 \ltdyn B_2$ that is not provable.
+\end{theorem}
+
+\begin{theorem}{Contextual Approximation}
+  If $\Gamma_1 \ltdyn \Gamma_2 \vdash M_1 \ltdyn M_2 : B_1 \ltdyn
+  B_2$, then for any context $C : (\Gamma_1 \vdash B_1) \Rightarrow
+  (\cdot \vdash \u F 2)$, and any valid interpretation of the dynamic
+  types, one of the following holds
+  \begin{enumerate}
+  \item $\sem{C[M_1]} \Downarrow \err$
+  \item $\sem{C[M_1]}, \sem{C[\dncast{B_1}{B_2}M_2[\upcast{\Gamma_1}{\Gamma_2}{\Gamma_1}]]} \Uparrow$
+  \item $\sem{C[M_1]},
+    \sem{C[\dncast{B_1}{B_2}M_2[\upcast{\Gamma_1}{\Gamma_2}{\Gamma_1}]]}
+    \Downarrow \ret V$ and $V = \tru$ or $V = \fls$.
+  \end{enumerate}
+\end{theorem}
 
 As described in the previous section, almost all of the contract
 translation is uniquely determined already: casts between function
@@ -1846,8 +1868,10 @@ covariant arguments of the opposite sort as the connective.
 %
 Because of this, they would need to be treated carefully, in a similar
 way as the $U, \u F$ connectives.
-v%
-In addition, the connectives are not operationally well-behaved.
+%
+In addition, the connectives do not seem to have an operational
+reading, or at least one that extends the call-by-push-value
+operational semantics.
 %
 For instance adding a value function space would mean also including a
 value application, and so operationally, values would not be inert.
@@ -1858,9 +1882,17 @@ and amenability to extensions.
 
 \appendix
 
-\section{Call-by-value Gradual Type Theory}
+In this appendix we present for the reader who is unfamiliar with
+call-by-push-value two type theories for call-by-value and
+call-by-name gradual typing in this style.
+%
+In each we prove one of the non-obvious uniqueness theorems that we
+showed for CBPV: in CBV we show the function type must be the
+thunkable, wrapping implementation and for the CBN what would we do??
+
+\section{Mini Call-by-value Gradual Type Theory}
 
-\section{Call-by-name Gradual Type Theory}
+\section{Mini Call-by-name Gradual Type Theory}
 
 \end{document}