typos

practical.tex

@@ -2,14 +2,14 @@ We have implemented a simplified version of the algorithm presented in
 Section~\ref{ssec:algorithm} that does
 not make use of type schemes and is, therefore, incomplete w.r.t. the
 system of Section~\ref{sec:static}. In particular, as we
-explained in Section~\ref{ssec:algorithm}, in the absence of type
+explained in Section~\ref{ssec:algorithm}, \beppe{did we?} in the absence of type
 schemes it is not always possible to prove that $\forall v, \forall t,
-v \in t \text{~or~} v \not\in \lnot t$. Since this property cease
+v \in t \text{~or~} v \not\in \lnot t$. Since this property ceases
 to hold only for $\lambda$-abstractions, then not using type schemes
 yields less precise typing only for tests $\ifty{e}t{e_1}{e_2}$ where $e$
 has a functional type, that is, the value tested will be a $\lambda$-abstraction.
 This seems like a reasonable compromise between the
-complexity of an implementation involving type scheme and the programs
+complexity of an implementation involving type schemes and the programs
 we want to type-check in practice. Indeed, if we restrict the language
 so that the only functional type $t$ allowed in a test $\ifty{e}t{e_1}{e_2}$
 is $\Empty{\to}\Any$---i.e., if we allow to check whether a value is a
@@ -22,7 +22,7 @@ algorithm defined on the base language, our implementation supports
 record types (Section \ref{ssec:struct}) and the refinement of function types
 (Section \ref{sec:refining} with the rule of Appendix~\ref{app:optimize}). The implementation is rather crude and
 consist of 2000 lines of OCaml code, including parsing, type-checking
-of programs and pretty printing of types. We demonstrate the output of
+of programs, and pretty printing of types. We demonstrate the output of
 our type-checking implementation in Table~\ref{tab:implem}. These
 examples and others can be tested in the online toplevel available at
 \url{https://occtyping.github.io/} (the corresponding repository is
@@ -162,7 +162,7 @@ since, \texttt{or\_} has type\\
 \centerline{$(\True\to\Any\to\True)\land(\Any\to\True\to\True)\land
    (\lnot\True\to\lnot\True\to\False)$}
 We consider \True, \Any and $\lnot\True$ as candidate types for
-\texttt{x} which, in turn allows us to deduce a precise type given in the table. Finally, thanks to this rule it is no longer necessary to force refinement by using a type case. As a consequence we can define the functions \texttt{and\_} and \texttt{xor\_} more naturally as:
+\texttt{x} which, in turn allows us to deduce a precise type given in the table. Finally, thanks to this rule it is no longer necessary to use a type case to force refinement. As a consequence we can define the functions \texttt{and\_} and \texttt{xor\_} more naturally as:
 \begin{alltt}\color{darkblue}\morecompact
 let and_ = fun (x : Any) -> fun (y : Any) -> not_ (or_ (not_ x) (not_ y))
 let xor_ = fun (x : Any) -> fun (y : Any) -> and_ (or_ x y) (not_ (and_ x y))

related.tex

@@ -41,3 +41,4 @@ pair. It is therefore unclear whether their systems allows one to
 write predicates over list types (e.g., test whether the input
 is a list of integers), which we can easily do thanks to our support
 for recursive types.\beppe{On peut dire plus? More generally, while their system refines only the type of variables, and only when they occur in some chosen contexts, our approach lifts this limitation on contexts and also refines the types of arbitrary expressions.} 
+\beppe{Est-ce vrai que: As far as we know, a code analysis such as the one performed by Code 8 for DOM objects is out of reach of the current occurrence typing state of the art.}