diff --git a/notes/gcbpv.tex b/notes/gcbpv.tex
index e1851743a3286ff12b709198432e12c4e5da9c83..4d2308648750f7956fc14a65faae00558b4c4f45 100644
--- a/notes/gcbpv.tex
+++ b/notes/gcbpv.tex
@@ -1112,7 +1112,7 @@ However, here is a more direct syntactic proof.
-\section{Models}
+\section{Concrete Syntactic Models}
To determine what sorts of dynamic type we want for different
applications, we consider the models.
@@ -1220,235 +1220,6 @@ Note that these both satisfy adjunction and retraction.
%% {{\lett y = \dncast{\u F T}{\u F \dynv}\ret x; \ret \roll\sigma_T y \ltdyn \ret x}}
\end{mathpar}
-\section{Call by Value $\ltdyn$ Call by Name}
-
-Can we model the idea that ``call by value errors more than call by
-name'' using type dynamism/ep pairs? Some basic calculations work
-out...
-
-\section{Focusing on an implementation}
-
-Call-by-push-value with complex values and stacks is odd from an
-operational perspective.
-%
-Values, rather than being simple trees built out of their
-constructors, can perform pattern matching on free variables, which
-would mean that they seemingly need ot be reduced operationally, when
-they are expected to be inert.
-%
-Dually, stacks, rather than being simple composites of
-\emph{destructors}, can also consist of $\lambda$s and code tuples,
-which are expected to \emph{delay} evaluation of their bodies in an
-operational semantics, whereas they are expected to \emph{force} the
-evaluation of the term plugged into the hole.
-%
-Levy resolves these seeming oddities by showing that as long as the
-values and stacks occur inside a larger term, the ``complex'' portions
-can be \emph{compiled away}.
-%
-Today, many years later, with the benefit of much hindsight, we can
-see Levy's proof as an application of the method of \emph{focusing}.
-
-Here we adapt that proof to get an operational semantics for
-\emph{Gradual} CBPV that will .
-%
-If we focus even more intensely we can make all upcasts between
-positive connectives implicit, but allowing positive variables rules
-out that possibility.
-
-\begin{figure}[H]
- \mbox{Values: $\Gamma \vdash V : A$}\\
- \begin{mathpar}
- \inferrule
- {\Gamma \vdash \hat V : A_1 \and A_1 \ltdyn A_2}
- {\Gamma \vdash \upcast {A_1}{A_2} \hat V : A_2}
- \end{mathpar}
- \mbox{Value Constructors: $\Gamma \vdash\hat V : A$}\\
- \begin{mathpar}
- \inferrule
- {x : A \in \Gamma}
- {\Gamma \vdash x : A}
-
- \inferrule
- {\Gamma \vdash V : A \and\Gamma \vdash V' : A'}
- {\Gamma \vdash ( V, V') : A \times A'}
-
- \inferrule
- {\Gamma \vdash V : A}
- {\Gamma \vdash \sigma_{A,A'} V : A + A'}
-
- \inferrule
- {\Gamma \vdash V' : A'}
- {\Gamma \vdash \sigma_{A,A'}' V' : A + A'}
-
- \inferrule
- {}
- {\Gamma \vdash () : 1}
-
- \inferrule
- {\Gamma \vdash M : \u B}
- {\Gamma \vdash \thunk M : U \u B}
- \end{mathpar}
-
- \mbox{Terms: $\Gamma \vdash M : \u B$}
- \begin{mathpar}
- \inferrule
- {}
- {\Gamma \vdash \err_{\u B} : \u B}
-
- \inferrule
- {\Gamma \vdash V : A}
- {\Gamma \vdash \ret V : \u F A}
-
- \inferrule
- {\Gamma \vdash V : U \u B\and
- \Gamma \pipe [ \u B ] \vdash S : \u C
- }
- {\Gamma \vdash \force V; S : \u B}
-
- \inferrule
- {\Gamma, x : A \vdash M : \u B}
- {\Gamma \vdash \lambda x : A. M : A \to \u B}
-
- \inferrule
- {}
- {\Gamma \vdash [] : \top}
-
- \inferrule
- {\Gamma \vdash M : \u B\and
- \Gamma \vdash M' : \u B'}
- {\Gamma \vdash [\pi \mapsto M \pipe \pi' \mapsto M'] : \u B \wedge \u B'}
-
- \inferrule
- {\Gamma \vdash V : A \times A'\and
- \Gamma, x : A, x': A' \vdash M : \u B}
- {\Gamma \vdash \lett (x,x') = V; M : \u B}
-
- \inferrule
- {\Gamma \vdash V : A + A'\and
- \Gamma , x:A \vdash M : \u B\and
- \Gamma , x:A' \vdash M' : \u B}
- {\Gamma \vdash \case V \{ \sigma x \mapsto M \pipe \sigma' x' \mapsto M' \} : \u B}
-
- \inferrule
- {\Gamma \vdash \hat M : \u B_2 \and \u B_1 \ltdyn \u B_2}
- {\Gamma \vdash \dncast{\u B_1}{\u B_2} \hat M : \u B_1}
- \end{mathpar}
-
- \mbox{Spines $\Gamma \pipe [ \u B ] \vdash S : \u C$}
- \begin{mathpar}
- \inferrule
- {\Gamma \pipe [ \u B_1] \vdash S : \u C \and \u B_1 \ltdyn \u B_2}
- {\Gamma \pipe [\u B_2] \vdash \dncast{\u B_1}{\u B_2}; S : \u C}
- \end{mathpar}
-
- \mbox{Computation Destructors $\Gamma\pipe [ \u B ] \vdash \hat S : \u C$}
- \begin{mathpar}
- \inferrule
- {}
- {\Gamma \pipe [\u B ] \vdash \bullet : \u B}
-
- \inferrule
- {\Gamma\pipe [\u B] \vdash S : \u C \and
- \Gamma \vdash V : A}
- {\Gamma\pipe [ A \to \u B ] \vdash 'V; S : \u C}
-
- \inferrule
- {\Gamma \pipe [\u B]\vdash S : C}
- {\Gamma \pipe [\u B \wedge \u B'] \vdash \pi; S : \u C}
-
- \inferrule
- {\Gamma \pipe [\u B']\vdash S : C}
- {\Gamma \pipe [\u B \wedge \u B'] \vdash \pi'; S : \u C}
-
- \inferrule
- {\Gamma, x : A \vdash M : \u C}
- {\Gamma \pipe [\u F A] \vdash \too x. M : \u C}
- \end{mathpar}
- \caption{Operational Gradual Call By Push Value (Sketchy)}
-\end{figure}
-
-\section{The Notes we Don't Play}
-
-From a ``completionist'' perspective, call-by-push-value is missing
-some interesting connectives that are easy to define.
-%
-When added to call-by-push-value, the language is called the enriched
-effect calculus (EEC) and has been studied extensively (cite).
-
-First, there are 3 missing multiplicative connectives: the pure
-function space $A \Rightarrow A'$, linear function space $\u B
-\multimap \u B'$ and tensor product of a value and computation type $A
-\otimes \u B$.
-%
-Since they are problematic I will only describe their sorts and their
-sequent calculus invertible rule:
-
-\begin{mathpar}
- \inferrule
- {A \vtype \and A' \vtype}
- {A \Rightarrow A' \vtype}
-
- \inferrule
- {\Gamma, A \vdash^V A'}
- {\Gamma \vdash^V A \Rightarrow A'}
-
- \inferrule
- {\u B \ctype \and \u B' \ctype}
- {\u B \multimap \u B' \vtype}
-
- \inferrule
- {\Gamma \pipe \u B \vdash \u B'}
- {\Gamma \vdash \u B \multimap \u B'}
-
- \inferrule
- {A \vtype \and \u B \ctype}
- {A \otimes \u B \ctype}
-
- \inferrule
- {\Gamma, A \pipe \u B \vdash \u C}
- {\Gamma \pipe A \otimes \u B \vdash \u C}
-\end{mathpar}
-
-First, they are ``boundary-crossing'' connectives in that they each
-have a \emph{covariant} argument whose sort is different from the sort
-of the constructor or a \emph{contravariant} argument whose sort is
-the same as the constructor.
-%
-The pure function space has a contravariant argument of the same sort,
-the linear function space has a covariant computation type argument
-while it is a value type and the value-computation tensor has a
-covariant value type argument while it is a computation type.
-
-Second, from the perspective of our focusing operational semantics,
-each of them violates the rule of our focusing system that the only
-negative value type is $U$ and the only positive computation type is
-$\u F$.
-%
-Note that this is similar to but not the same as the boundary crossing
-rule, and there are some \emph{additives} that we violate the focusing
-restriction but not the boundary-crossing restriction: the negative
-value product and the positive computation sum, which we show now.
-
-\begin{mathpar}
- \inferrule
- {A \vtype \and A' \vtype}
- {A \& A' \vtype}
-
- \inferrule
- {\Gamma \vdash A \and \Gamma \vdash A'}
- {\Gamma \vdash A \& A'}
-
- \inferrule
- {\u B \ctype \and \u B' \ctype}
- {\u B \oplus \u B' \ctype}
-
- \inferrule
- {{\Gamma \pipe \u B \vdash \u C} \and
- {\Gamma \pipe \u B' \vdash \u C}}
- {\Gamma \pipe \u B \oplus \u B' \vdash \u C}
-\end{mathpar}
-
\end{document}
%% Local Variables:
diff --git a/notes/operational-gtt.tex b/notes/operational-gtt.tex
new file mode 100644
index 0000000000000000000000000000000000000000..e7fb05cdf6b482ae90d57aed085b23065a6ccaa2
--- /dev/null
+++ b/notes/operational-gtt.tex
@@ -0,0 +1,222 @@
+\section{Focusing on an implementation}
+
+Call-by-push-value with complex values and stacks is odd from an
+operational perspective.
+%
+Values, rather than being simple trees built out of their
+constructors, can perform pattern matching on free variables, which
+would mean that they seemingly need ot be reduced operationally, when
+they are expected to be inert.
+%
+Dually, stacks, rather than being simple composites of
+\emph{destructors}, can also consist of $\lambda$s and code tuples,
+which are expected to \emph{delay} evaluation of their bodies in an
+operational semantics, whereas they are expected to \emph{force} the
+evaluation of the term plugged into the hole.
+%
+Levy resolves these seeming oddities by showing that as long as the
+values and stacks occur inside a larger term, the ``complex'' portions
+can be \emph{compiled away}.
+%
+Today, many years later, with the benefit of much hindsight, we can
+see Levy's proof as an application of the method of \emph{focusing}.
+
+Here we adapt that proof to get an operational semantics for
+\emph{Gradual} CBPV that will .
+%
+If we focus even more intensely we can make all upcasts between
+positive connectives implicit, but allowing positive variables rules
+out that possibility.
+
+\begin{figure}[H]
+ \mbox{Values: $\Gamma \vdash V : A$}\\
+ \begin{mathpar}
+ \inferrule
+ {\Gamma \vdash \hat V : A_1 \and A_1 \ltdyn A_2}
+ {\Gamma \vdash \upcast {A_1}{A_2} \hat V : A_2}
+ \end{mathpar}
+ \mbox{Value Constructors: $\Gamma \vdash\hat V : A$}\\
+ \begin{mathpar}
+ \inferrule
+ {x : A \in \Gamma}
+ {\Gamma \vdash x : A}
+
+ \inferrule
+ {\Gamma \vdash V : A \and\Gamma \vdash V' : A'}
+ {\Gamma \vdash ( V, V') : A \times A'}
+
+ \inferrule
+ {\Gamma \vdash V : A}
+ {\Gamma \vdash \sigma_{A,A'} V : A + A'}
+
+ \inferrule
+ {\Gamma \vdash V' : A'}
+ {\Gamma \vdash \sigma_{A,A'}' V' : A + A'}
+
+ \inferrule
+ {}
+ {\Gamma \vdash () : 1}
+
+ \inferrule
+ {\Gamma \vdash M : \u B}
+ {\Gamma \vdash \thunk M : U \u B}
+ \end{mathpar}
+
+ \mbox{Terms: $\Gamma \vdash M : \u B$}
+ \begin{mathpar}
+ \inferrule
+ {}
+ {\Gamma \vdash \err_{\u B} : \u B}
+
+ \inferrule
+ {\Gamma \vdash V : A}
+ {\Gamma \vdash \ret V : \u F A}
+
+ \inferrule
+ {\Gamma \vdash V : U \u B\and
+ \Gamma \pipe [ \u B ] \vdash S : \u C
+ }
+ {\Gamma \vdash \force V; S : \u B}
+
+ \inferrule
+ {\Gamma, x : A \vdash M : \u B}
+ {\Gamma \vdash \lambda x : A. M : A \to \u B}
+
+ \inferrule
+ {}
+ {\Gamma \vdash [] : \top}
+
+ \inferrule
+ {\Gamma \vdash M : \u B\and
+ \Gamma \vdash M' : \u B'}
+ {\Gamma \vdash [\pi \mapsto M \pipe \pi' \mapsto M'] : \u B \wedge \u B'}
+
+ \inferrule
+ {\Gamma \vdash V : A \times A'\and
+ \Gamma, x : A, x': A' \vdash M : \u B}
+ {\Gamma \vdash \lett (x,x') = V; M : \u B}
+
+ \inferrule
+ {\Gamma \vdash V : A + A'\and
+ \Gamma , x:A \vdash M : \u B\and
+ \Gamma , x:A' \vdash M' : \u B}
+ {\Gamma \vdash \case V \{ \sigma x \mapsto M \pipe \sigma' x' \mapsto M' \} : \u B}
+
+ \inferrule
+ {\Gamma \vdash \hat M : \u B_2 \and \u B_1 \ltdyn \u B_2}
+ {\Gamma \vdash \dncast{\u B_1}{\u B_2} \hat M : \u B_1}
+ \end{mathpar}
+
+ \mbox{Spines $\Gamma \pipe [ \u B ] \vdash S : \u C$}
+ \begin{mathpar}
+ \inferrule
+ {\Gamma \pipe [ \u B_1] \vdash S : \u C \and \u B_1 \ltdyn \u B_2}
+ {\Gamma \pipe [\u B_2] \vdash \dncast{\u B_1}{\u B_2}; S : \u C}
+ \end{mathpar}
+
+ \mbox{Computation Destructors $\Gamma\pipe [ \u B ] \vdash \hat S : \u C$}
+ \begin{mathpar}
+ \inferrule
+ {}
+ {\Gamma \pipe [\u B ] \vdash \bullet : \u B}
+
+ \inferrule
+ {\Gamma\pipe [\u B] \vdash S : \u C \and
+ \Gamma \vdash V : A}
+ {\Gamma\pipe [ A \to \u B ] \vdash 'V; S : \u C}
+
+ \inferrule
+ {\Gamma \pipe [\u B]\vdash S : C}
+ {\Gamma \pipe [\u B \wedge \u B'] \vdash \pi; S : \u C}
+
+ \inferrule
+ {\Gamma \pipe [\u B']\vdash S : C}
+ {\Gamma \pipe [\u B \wedge \u B'] \vdash \pi'; S : \u C}
+
+ \inferrule
+ {\Gamma, x : A \vdash M : \u C}
+ {\Gamma \pipe [\u F A] \vdash \too x. M : \u C}
+ \end{mathpar}
+ \caption{Operational Gradual Call By Push Value (Sketchy)}
+\end{figure}
+
+\section{The Notes we Don't Play}
+
+From a ``completionist'' perspective, call-by-push-value is missing
+some interesting connectives that are easy to define.
+%
+When added to call-by-push-value, the language is called the enriched
+effect calculus (EEC) and has been studied extensively (cite).
+
+First, there are 3 missing multiplicative connectives: the pure
+function space $A \Rightarrow A'$, linear function space $\u B
+\multimap \u B'$ and tensor product of a value and computation type $A
+\otimes \u B$.
+%
+Since they are problematic I will only describe their sorts and their
+sequent calculus invertible rule:
+
+\begin{mathpar}
+ \inferrule
+ {A \vtype \and A' \vtype}
+ {A \Rightarrow A' \vtype}
+
+ \inferrule
+ {\Gamma, A \vdash^V A'}
+ {\Gamma \vdash^V A \Rightarrow A'}
+
+ \inferrule
+ {\u B \ctype \and \u B' \ctype}
+ {\u B \multimap \u B' \vtype}
+
+ \inferrule
+ {\Gamma \pipe \u B \vdash \u B'}
+ {\Gamma \vdash \u B \multimap \u B'}
+
+ \inferrule
+ {A \vtype \and \u B \ctype}
+ {A \otimes \u B \ctype}
+
+ \inferrule
+ {\Gamma, A \pipe \u B \vdash \u C}
+ {\Gamma \pipe A \otimes \u B \vdash \u C}
+\end{mathpar}
+
+First, they are ``boundary-crossing'' connectives in that they each
+have a \emph{covariant} argument whose sort is different from the sort
+of the constructor or a \emph{contravariant} argument whose sort is
+the same as the constructor.
+%
+The pure function space has a contravariant argument of the same sort,
+the linear function space has a covariant computation type argument
+while it is a value type and the value-computation tensor has a
+covariant value type argument while it is a computation type.
+
+Second, from the perspective of our focusing operational semantics,
+each of them violates the rule of our focusing system that the only
+negative value type is $U$ and the only positive computation type is
+$\u F$.
+%
+Note that this is similar to but not the same as the boundary crossing
+rule, and there are some \emph{additives} that we violate the focusing
+restriction but not the boundary-crossing restriction: the negative
+value product and the positive computation sum, which we show now.
+
+\begin{mathpar}
+ \inferrule
+ {A \vtype \and A' \vtype}
+ {A \& A' \vtype}
+
+ \inferrule
+ {\Gamma \vdash A \and \Gamma \vdash A'}
+ {\Gamma \vdash A \& A'}
+
+ \inferrule
+ {\u B \ctype \and \u B' \ctype}
+ {\u B \oplus \u B' \ctype}
+
+ \inferrule
+ {{\Gamma \pipe \u B \vdash \u C} \and
+ {\Gamma \pipe \u B' \vdash \u C}}
+ {\Gamma \pipe \u B \oplus \u B' \vdash \u C}
+\end{mathpar}