some notation for lr and get it to compile

paper/gtt.tex

@@ -10,6 +10,7 @@
 %% 'sigplan,10pt'.
 
 %% Some recommended packages.
+\usepackage{mathpartir}
 % \usepackage{booktabs}   %% For formal tables:
 %                         %% http://ctan.org/pkg/booktabs
 % \usepackage{subcaption} %% For complex figures with subfigures/subcaptions
@@ -122,6 +123,14 @@
 \newcommand{\equidyn}{\mathrel{\gtdyn\ltdyn}}
 \newcommand{\ltdynv}{\mathrel{\sqsubseteq_V}}
 \newcommand{\ltdynt}{\mathrel{\sqsubseteq_T}}
+\newcommand{\ltlogty}[2]{\mathrel{\ltdyn^{#1}_{#2}}}
+\newcommand{\ltlogc}[1]{\mathrel{\ltdyn^{#1}_{\vdash}}}
+\newcommand{\ltdynlt}{\mathrel{\sqsubseteq\prec}}
+\newcommand{\ltdyngt}{\mathrel{\sqsubseteq\succ}}
+\newcommand{\ltltlogty}[2]{\mathrel{\ltdynlt^{#1}_{#2}}}
+\newcommand{\ltgtlogty}[2]{\mathrel{\ltdyngt^{#1}_{#2}}}
+\newcommand{\ltltlogc}[1]{\mathrel{\ltdynlt^{#1}_{\vdash}}}
+\newcommand{\ltgtlogc}[1]{\mathrel{\ltdyngt^{#1}_{\vdash}}}
 
 \newcommand{\pair}[2]{\{ \pi \mapsto {#1} \pipe \pi' \mapsto {#2}\}}
 
@@ -133,6 +142,7 @@
 \newcommand{\upcast}[2]{\langle{#2}\uarrow{#1}\rangle}
 \newcommand{\dncast}[2]{\langle{#1}\darrow{#2}\rangle}
 \newcommand{\err}{\mho}
+\newcommand{\print}{\text{print}\,\,}
 \newcommand{\roll}{\text{roll}\,\,}
 \newcommand{\unroll}{\text{unroll}\,\,}
 
@@ -446,7 +456,7 @@ the same stack.
 \begin{mathpar}
   \inferrule
   {\Gamma \pipe \u B \vdash S : \u C}
-  {\Gamma \vdash S[\error] \equidyn \error}
+  {\Gamma \vdash S[\err] \equidyn \err}
 
   \inferrule
   {\Gamma \pipe \u B \vdash S : \u C \and \Gamma \vdash M : \u B \and \Gamma \vdash V : \texttt{Char}}
@@ -490,7 +500,7 @@ 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$
+for every such pair, we add an upcast from $A$ to $B$: $\upcast 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
@@ -546,12 +556,19 @@ 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
+In a language with effects, 
 
 The na\"ive casts are also problemantic syntactically.
 %
 The first issue is that they violate a type theoretic principle of
-\emph{modularity}: 
+\emph{modularity}: every construction of the language should be
+independent of the presence of any other.
+%
+In this case, the na\"ive casts all violate this principle because the
+casts for value types use $\u F$ and the casts for computation types
+use $U$.
+%
+TODO: do we actually know what would go wrong in that case?
 
 %% Counterexample
 
@@ -606,7 +623,11 @@ consequences.
 
 
 \begin{figure}
-  
+  \begin{mathpar}
+    {\ltltlogty{i}{A}},{\ltgtlogty{i}{A}} \subseteq \{ \cdot \vdash V : A \}^2\\
+    {\ltltlogty{i}{\u B}},{\ltgtlogty{i}{\u B}} \subseteq \{ \cdot \pipe \u B \vdash S : \u F (1 + 1) \}^2\\
+    {\ltltlogc{i}}, {\ltgtlogc{i}} \subseteq \{ \cdot \vdash M : \u F (1 + 1) \}^2\\\\
+  \end{mathpar}
   \caption{Observational Approximation Logical Relation}
 \end{figure}