typos

Makefile

 default:
-	latexmk -pdf -bibtex main.tex
+	latexmk -pdf -bibtex main-elsarticle.tex
 
 
 

intro.tex

@@ -37,7 +37,7 @@ Occurrence typing was first defined and formally studied by
 programs,\footnote{%
 According to Sam Tobin-Hochstadt, the terminology \emph{occurrence
 typing} was first used in a simplistic form by~\citet{Komon05},
-although he was not aware of it the at the moment of
+although he and Felleisen were not aware of it the at the moment of
 the writing of~\cite{THF08}.}
 and later extended by \citet{THF10}
 yielding the development of Typed Racket. From its inception,

practical.tex

@@ -30,8 +30,9 @@ memoization environment in the code of the $\Refine {e,t}{\Gamma}$
 function, which allows the inference to avoid unnecessary traversals
 of $e$.
 Lastly, while our prototype allows the user to specify a particular
-value for the $n_0$ parameter, the default value of $1$ is sufficient
-to check all examples we present in the following sections.
+value for the $n_o$ parameter we introduced in
+Section~\ref{sec:typenv}, a value of $1$ for $n_o$ is sufficient
+to check all examples we present in the rest of the section.
 }
 
 \subsection{Experiments}

related.tex

@@ -364,28 +364,30 @@ test how much of their analysis we can capture and enhance by
 formalizing it in our system.
 \nocite{typescript,flow}
 \rev{%%%
-More generally, we believe that what sets apart our work in the
-palimpsest of the research on occurrence typing is that we have a type-theoretic
-foundational approach striving as much as possible to explain
-occurrence typing by extending prior (unrelated but standard) work
-while keeping prior results. In that respect, we think that our
+More generally, we believe that what sets our work apart in the
+palimpsest of the research on occurrence typing is that we have a
+type-theoretic foundational approach striving as much as possible to
+explain occurrence typing by extending prior (unrelated but standard)
+work while keeping prior results. In that respect, we think that our
 approach is not satisfactory, yet, because it uses non standard
-type-environments that map expressions rather than variables to
-types: but all the rest is standard type-theory. And even on the latter
+type-environments that map expressions rather than variables to types:
+but all the rest is standard type-theory. And even on the latter
 aspect it must be recognized that the necessity of tracking types not
 only for variables but also for more structured expressions is
 something that shows up, in different forms, in several other
 approaches. For instance, in the approach defined for Typed
 Racket~\cite{THF10} the type-system associates to an expression a
-quadruple formed by its type, two logical propositions, and an object which is
-a pointer to the environment for the type hypothesis about the
-expression and, as such, it plays the role of our extended type
+quadruple formed by its type, two logical propositions, and an object
+which is a pointer to the environment for the type hypothesis about
+the expression and, as such, it plays the role of our extended type
 environments. Likewise, the \emph{selfification} of \cite{OTMW04}
 and \cite{KF09}, propagates the precise type constraints learned
 during a test. However, in the latter, whole the information can be
 kept at the type level, since dependent types contains terms and can
-introduce variables, while in our approach the mapping is kept in an environment.
-Nevertheless, we are confident that even this last non-standard aspect
+introduce variables, while in our approach the mapping is kept in an
+environment.  The tracking of types for structured expressions thus
+seems a common aspect of different approaches to occurrence types,
+nevertheless we are confident that even this last non-standard aspect
 of our system can be removed and that occurrence typing can be
 explained in a pure standard type-theoretic setting.