diff --git a/jfp-paper/defs.tex b/jfp-paper/defs.tex
index 6f1ee2de1fc5fd2aed6a7b5353c6b226431caf58..ab761f10810f794e482881a37af72b57f097a574 100644
--- a/jfp-paper/defs.tex
+++ b/jfp-paper/defs.tex
@@ -24,7 +24,7 @@
 \newcommand{\cbpv}{CBPV}
 \newcommand{\cbpvstar}{CBPV*}
 \newcommand{\cbpvtxt}{\cbpv}
-\newcommand{\sem}[1]{[[#1]]}
+\newcommand{\sem}[1]{\llbracket{#1}\rrbracket}
 \newcommand{\sdncast}[2]{\sem{\dncast{#1}{#2}}}
 \newcommand{\supcast}[2]{\sem{\upcast{#1}{#2}}}
 \newcommand{\srho}[1]{\sem{#1}_\rho}
@@ -159,8 +159,9 @@
 \newcommand\errordivergeright[0]{\ltdyn\succeq}
 \newcommand\errordivergerightop[0]{\preceq\gtdyn}
 
-\newcommand\bvtopv[1]{#1^{c}}
-\newcommand\bvtopvpure[1]{#1^{v}}
+\newcommand\cbvtocbpvcomp[1]{#1^{c}}
+\newcommand\cbvtocbpvval[1]{#1^{v}}
+\newcommand\cbvtocbpvty[1]{#1^{ty}}
 \newcommand\purely{\downarrow}
 
 %% Local Variables:
diff --git a/jfp-paper/jfp-gtt.tex b/jfp-paper/jfp-gtt.tex
index 62a0a782162e15254a34cf560438fe4344fb5811..b6826a7d7cf7bd736a48d8619499678c550e0911 100644
--- a/jfp-paper/jfp-gtt.tex
+++ b/jfp-paper/jfp-gtt.tex
@@ -4,8 +4,8 @@
 \newif\ifshort
 \newif\iflong
 %% Pick long or short version:
-%% \shorttrue
-\longtrue
+\shorttrue
+%% \longtrue
 
 \usepackage{amssymb}
 %% \usepackage{amsthm}
@@ -3939,6 +3939,143 @@ Theorem~\ref{thm:monadic-comonadic-casts} gives the result.
 %% In order for this duality to be \emph{perfect}, we use the version of
 %% casts that are \emph{not} assumed to be 
 
+\section{Application: Deriving Call-by-value Operational Semantics}
+
+To show how GTT can be used to inform language design, we show how the
+uniqueness principles of Theorem~\ref{thm:casts-unique} justify most
+of the operational behavior of a standard Call-by-value cast calculus.
+
+\begin{figure}
+  \begin{mathpar}
+    \begin{array}{lrcl}
+      \mbox{Types} & A & \bnfdef &
+    {\dyn} \alt {A \to A} \alt {1}\alt {A \times A}\alt 0 \alt {A + A}\\
+      \mbox{Tags} & G & \bnfdef & \dyn \to \dyn \alt 1 \alt \dyn \times \dyn \alt 0 \alt \dyn + \dyn\\
+      \mbox{Terms} & M,N & \bnfdef &
+      \err \alt x \alt
+      \obcast{A}{A}M\alt
+      () \alt \pmpairWtoinZ M N\alt
+      (M,N) \alt \pmpairWtoXYinZ M x y N\\
+      & & \alt &
+      \inl M\alt \inr M\alt
+      \caseofXthenYelseZ M {x_1. N_1}{x_2. N_2} \alt
+      \lambda x:A. M \alt M\,N\\
+
+      \mbox{Values} & V & \bnfdef &
+      \obcast G \dyn V \alt \lambda x:A. M \alt () \alt (V,V) \alt \inl V \alt \inr V \\
+    \mbox{Evaluation Contexts} & S & \bnfdef &
+    \bullet \alt \obcast B A S\alt
+    (S,N)\alt (M, S) \alt \pmpairWtoXYinZ S x y N\\
+    &&\alt&
+    \inl S \alt \inr S \alt \caseofXthenYelseZ S {x_1.N_1}{x_2.N_2}\alt
+    S\,N\alt V\,S\\
+    \mbox{Environments} & \Gamma & \bnfdef & \cdot \alt \Gamma,x:A\\
+    \mbox{Substitutions} & \gamma & \bnfdef & \cdot \alt \gamma, V/x
+    \end{array}
+  \end{mathpar}
+  \caption{CBV Cast Calculus}
+\end{figure}
+
+\begin{figure}
+  \begin{mathpar}
+    E[\letXbeYinZ V x N] \step E[N[V/x]]\and
+    E[(\lambda x:A. M)\,V] \step E[M[V/x]]\and
+    E[\pmpairWtoinZ V N] \step E[N]\and
+    E[\pmpairWtoXYinZ {(V_1,V_2)} {x_1}{x_2} N] \step E[N[V_1/x_1][V_2/x_2]]\and
+    E[\caseofXthenYelseZ {\inl V}{x_1. N_1}{x_2. N_2}] \step E[N_1[V/x_1]]\and
+    E[\caseofXthenYelseZ {\inr V}{x_1. N_1}{x_2. N_2}] \step E[N_2[V/x_2]]\\\\
+    \inferrule
+    {}
+    {\obcast{\dyn}{\dyn}V \step E[V]}\and
+    \inferrule
+    {A \ltdyn G}
+    {E[\obcast \dyn A V] \step E[\obcast{\dyn}{G}\obcast{G}{A}V]}\and
+    \inferrule
+    {A \ltdyn G}
+    {E[\obcast A \dyn V] \step E[\obcast A G \obcast G \dyn V]}\and
+    \inferrule
+    {}
+    {E[\obcast G \dyn \obcast \dyn G V] \step E[V]}\and
+    \inferrule
+    {G \neq G'}
+    {E[\obcast {G'} \dyn \obcast \dyn {G} ]}\and
+    \inferrule
+    {A \ltdyn G_A \and B \ltdyn G_B \and G_A \neq G_B}
+    {E[\obcast B A V] \step \err}\and
+    \inferrule
+    {}
+    {E[\obcast{A_1' \to A_2'}{A_1 \to A_2}V]\step
+     E[\lambda x:A_1'. \obcast{A_2'}{A_2}(V\,(\obcast{A_1}{A_1'}x))]}\and
+    \inferrule
+    {}
+    {E[\obcast 1 1 ()] \step E[()]}\and
+    \inferrule
+    {}
+    {E[\obcast{A_1' \times A_2'}{A_1 \times A_2}(V_1,V_2)] \step
+     E[(\obcast{A_1'}{A_1}V_1,\obcast{A_2'}{A_2}V_2)]}\and
+    \inferrule
+    {}
+    {E[\obcast{A_1' + A_2'}{A_1 + A_2}{(\inl V)}]\step
+    E[\obcast{A_1'}{A_1}V]}\and
+    \inferrule
+    {}
+    {E[\obcast{A_1' + A_2'}{A_1 + A_2}{(\inr V)}]\step
+    E[\obcast{A_2'}{A_2}V]}
+  \end{mathpar}
+  \caption{CBV Cast Calculus Operational Semantics}
+\end{figure}
+
+\begin{figure}
+  \begin{align*} % ?, ->, 1, *, 0, +
+    \cbvtocbpvty{\dyn} &= \dyn\\
+    \cbvtocbpvty{(A \to A')} &= \cbvtocbpvty{A} \to \cbvtocbpvty{A'}\\
+    \cbvtocbpvty{1} &= 1\\
+    \cbvtocbpvty{(A_1 \times A_2)} &= \cbvtocbpvty{A_1} \times \cbvtocbpvty{A_2}\\
+    \cbvtocbpvty{0} &= 0\\
+    \cbvtocbpvty{(A_1 + A_2)} &= \cbvtocbpvty{A_1} + \cbvtocbpvty{A_2}\\\\
+    \cbvtocbpvcomp{x} &= \ret x\\
+    \cbvtocbpvcomp{(\letXbeYinZ M x N)} &=
+    \bindXtoYinZ {\cbvtocbpvcomp{M}} x {\cbvtocbpvcomp{N}}\\
+    \cbvtocbpvcomp{(\obcast{A_2}{A_1}M)} &=
+    \bindXtoYinZ M x
+    \dncast{F \cbvtocbpvty{A_2}}{F \dyn}{(\ret {\upcast{\cbvtocbpvty{A_1}}{\dyn}x})}\\
+    \cbvtocbpvcomp{(\lambda x:A. M)} &=
+    \ret (\thunk {(\lambda x:\cbvtocbpvty{A}. \cbvtocbpvcomp{M})})\\
+    \cbvtocbpvcomp{(M\,N)} &=
+    \bindXtoYinZ {\cbvtocbpvcomp M} f
+    \bindXtoYinZ {\cbvtocbpvcomp N} x
+    \force f\,x\\
+    \cbvtocbpvcomp{()} &= \ret ()\\
+    \cbvtocbpvcomp{(\pmpairWtoinZ M N)} &=
+    \bindXtoYinZ {\cbvtocbpvcomp M} z \pmpairWtoinZ z N\\
+    \cbvtocbpvcomp{(M_1,M_2)} &=
+    \bindXtoYinZ {\cbvtocbpvcomp {M_1}} {x_1}
+    \bindXtoYinZ {\cbvtocbpvcomp {M_2}} {x_2}
+    \ret (x_1,x_2)\\
+    \cbvtocbpvcomp{(\pmpairWtoXYinZ M x y N)} &=
+    \bindXtoYinZ {\cbvtocbpvcomp M} z
+    \pmpairWtoXYinZ z x y {\cbvtocbpvcomp N}\\
+    \cbvtocbpvcomp{(\abort M)} &=
+    \bindXtoYinZ {\cbvtocbpvcomp M} z {\abort z}\\
+    \cbvtocbpvcomp{(\inl M)} &=
+    \bindXtoYinZ {\cbvtocbpvcomp{M}} x \ret \inl x\\
+    \cbvtocbpvcomp{(\inr M)} &=
+    \bindXtoYinZ {\cbvtocbpvcomp{M}} x \ret \inr x\\
+    \cbvtocbpvcomp{(\caseofXthenYelseZ M {x_1. N_1}{x_2. N_2})} &=
+    \bindXtoYinZ {\cbvtocbpvcomp M} z
+    \caseofXthenYelseZ z {x_1. \cbvtocbpvcomp {N_1}}{x_2. \cbvtocbpvcomp {N_2}}\\\\
+    \cbvtocbpvval{(\obcast{\dyn}{G}V)} &= \upcast{\cbvtocbpvty{G}}{\dyn}V\\
+    \cbvtocbpvval{(\lambda x:A. M)} &=
+    \thunk {(\lambda x:\cbvtocbpvty{A}. \cbvtocbpvcomp{M})}\\
+    \cbvtocbpvval{()} &= ()\\
+    \cbvtocbpvval{(V_1,V_2)} &= (\cbvtocbpvval {V_1}, \cbvtocbpvval {V_2})\\
+    \cbvtocbpvval{(\inl V)} &= \inl \cbvtocbpvval V \\
+    \cbvtocbpvval{(\inr V)} &= \inr \cbvtocbpvval V \\
+  \end{align*}
+  \caption{CBV to GTT translation}
+\end{figure}
+
+
 \section{Contract Models of GTT}
 \label{sec:contract}