Shaving a few lines and fixing typos.

code_table.tex

 \lstset{language=[Objective]Caml,columns=fixed,basicstyle=\linespread{0.43}\ttfamily\scriptsize,aboveskip=-0.5em,belowskip=-1em,xleftmargin=-0.5em}
 \begin{table}
    {\scriptsize
-  \begin{tabular}{|@{\,}c@{\,}|p{0.482\textwidth}@{}|@{\,}p{0.482\textwidth}@{\,}|}
+  \begin{tabular}{|@{\,}c@{\,}|p{0.54\textwidth}@{}|@{\,}p{0.41\textwidth}@{\,}|}
 \hline
     & Code & Inferred type\\
-    \hline
+%    \hline
     \hline
     1 &
           \begin{lstlisting}
@@ -84,7 +84,8 @@ $(\lnot(\Int \lor \Char) \to (\Int \to 2) \land
           (\lnot\Int \to 3) \land$\newline
 \hspace*{0.2cm}$(\Bool \to 3) \land(\lnot(\Bool \lor \Int) \to 3)
           \land (\lnot\Bool \to 2
-          \lor 3))$~~$\land \ldots$ (two other redundant cases omitted)
+                  \lor 3))$\newline
+                  $\land \ldots$ (two other redundant cases omitted)
 %                   \newline
 % $(\lnot\Char \to (\Int \to 2) \land (\lnot\Int \to 1 \lor 3) \land (\Bool \to 1 \lor 3) \land$\newline
 % \hspace*{1cm}$(\lnot(\Bool \lor \Int) \to 3) \land
@@ -106,10 +107,9 @@ let test_3 = f nil nil
     8 &
 \begin{lstlisting}
 type Document = { nodeType=9 ..}
-and Element  = { childNodes=NodeList,
-                 nodeType=1 ..}
-and Text = { isElementContentWhiteSpace=Bool,
-             nodeType=3, ..}
+and Element = { nodeType=1, childNodes=NodeList ..}
+and Text = { nodeType=3,
+             isElementContentWhiteSpace=Bool ..}
 and Node = Document | Element | Text
 and NodeList = Nil | (Node, NodeList)
 
@@ -119,10 +119,13 @@ let is_empty_node = fun (x : Node) ->
     x.isElementContentWhiteSpace
   else
   if x.childNodes is Nil then true else false
-\end{lstlisting} &\vspace{19mm}
+\end{lstlisting} &\vspace{12mm}
 $(\Keyw{Document}\to\False)~\land$\newline
 $(\orecord{ \texttt{nodeType}\,{=}\,1, \texttt{childNodes}\,{=}\,\Keyw{Nil} }\to\True) ~\land$\newline
-$(\orecord{ \texttt{nodeType}\,{=}\,1, \texttt{childNodes}\,{=}\,(\Keyw{Node},\Keyw{NodeList}) }\to\False) ~\land$\newline
+$(\orecord{ \texttt{nodeType}\,{=}\,1,
+                   \texttt{childNodes}\,{=}\,(\Keyw{Node},\Keyw{NodeList})
+                   }$\newline
+                   \hspace*{4.5cm}$\to\False) ~\land$\newline
 $(\Keyw{Text}\to\Bool)~\land$\newline (omitted redundant arrows)
     \\\hline
     9 & \begin{lstlisting}
@@ -145,6 +148,6 @@ $(\Int\to\textsf{Empty})\land(\neg\Int\to{}2)$\newline
     \\\hline
   \end{tabular}
 }
-\caption{Types inferred by implementation}\vspace{-10mm}
+\caption{Types inferred by the implementation}\vspace{-10mm}
 \label{tab:implem}
 \end{table}

gradual.tex

@@ -18,13 +18,13 @@ instance, the JavaScript code of~\eqref{foo} and~\eqref{foo2} in the introductio
 typed by using gradual typing:\vspace{-.4mm}
 \begin{alltt}\color{darkblue}\morecompact
   function foo(x\textcolor{darkred}{ : \pmb{\dyn}}) \{
-      return (typeof(x) === "number")? x++ : x.trim()  \refstepcounter{equation}                                \mbox{\color{black}\rm(\theequation)}\label{foo3}
+      return (typeof(x) === "number")? x++ : x.trim();  \refstepcounter{equation}                                \mbox{\color{black}\rm(\theequation)}\label{foo3}
   \}\negspace
 \end{alltt}
 ``Standard'' gradual typing inserts two dynamic checks since it compiles the code above into:
 \begin{alltt}\color{darkblue}\morecompact
   function foo(x) \{
-      return (typeof(x) === "number")? (\textcolor{darkred}{\Cast{number}{{\color{darkblue}x}}})++ : (\textcolor{darkred}{\Cast{string}{{\color{darkblue}x}}}).trim()
+      return (typeof(x) === "number")? (\textcolor{darkred}{\Cast{number}{{\color{darkblue}x}}})++ : (\textcolor{darkred}{\Cast{string}{{\color{darkblue}x}}}).trim();
   \}\negspace
 \end{alltt}
 where {\Cast{$t$}{$e$}} is a type-cast that dynamically checks whether the value returned by $e$ has type $t$.\footnote{Intuitively, \code{\Cast{$t$}{$e$}} is

practical.tex

@@ -118,7 +118,7 @@ type depending on whether the content of the \texttt{childNodes} field
 is the empty list or not.
 
 Code~9 shows the usefulness of the rule \Rule{OverApp}.
-Consider the definition of the \texttt{xor\_} operator (Code~9).
+Consider the definition of the \texttt{xor\_} operator.
 Here the rule~[{\sc AbsInf}+] is not sufficient to precisely type the
 function, and using only this rule would yield a type
  $\Any\to\Any\to\Bool$.
@@ -132,7 +132,7 @@ Let us follow the behavior of the
  ``\texttt{then}'' branch is $\True\vee\lnot\True\lor\True\simeq\Any$,
 and a similar reasoning holds for \texttt{y}. 
 \fi%%%%%%%%%%%%%%
-However, since in Code~9 \texttt{or\_} has type
+However, since \texttt{or\_} has type
 %\\[.7mm]\centerline{%
 $(\True\to\Any\to\True)\land(\Any\to\True\to\True)\land
    (\lnot\True\to\lnot\True\to\False)$