typos

practical.tex

@@ -25,9 +25,9 @@ types. \rev{CDuce is used as a library to provide set-theoretic types and
 semantic subtyping. The implementation faithfully transcribe in OCaml
 the algorithmic system $\vdashA$ as well as all the type operations
 defined in this work. One optimization that our implementation
-features (w.r.t to the formal presentation) is the use of a
+features (with respect to the formal presentation) is the use of a
 memoization environment in the code of the $\Refine {e,t}{\Gamma}$
-function, that allows to avoid several traversal of $e$.
+function, that avoids unnecessary traversals of $e$.
 }
 
 \subsection{Experiments}
@@ -262,7 +262,7 @@ let get_property_l =
 \end{alltt}
 where  \code{\textit{S}} is \code{Object} and  \code{\textit{T}} is \code{Any}.
 
-\subsection{Comparison with \cite{THF10}}
+\subsection{Comparison}
 
 \input{code_table2}
 In Table~\ref{tab:implem2}, we reproduce in our syntax the 14

related.tex

@@ -256,7 +256,7 @@ of Dminor refines the type of each branch by remembering that $e$
 (resp. $\lnot e$) is true in $e_1$ (resp. $e_2$) and this information
 is not propagated to the outer context.
 A similar approach is taken by \citet{Chugh12}, and extended to so-called nested refinement types. In these types, an arrow type may
-appear in a logical formula (where previous work only allowed formulae
+appear in a logical formula (whereas previous work only allowed formulae
 on  ``base types''). This is done in the context of a dynamic
 language and their approach is extended with polymorphism, dynamic
 dispatch and record types.