typeos

related.tex

@@ -85,9 +85,9 @@ by skipping the typing of non-selectable branches. They use this
 second type system only to prove type preservation and obtain, thus,
 the soundness of their type system. In our work, instead, we prefer to
 start directly with a system that satisfies type preservation. Our
-system does not have the problem the first system of~\cite{THF08}
+system does not have the problem of the first system of~\cite{THF08}
 thanks to the
-presence the \Rule{Efq} rule that we included for that very purpose,
+presence of the \Rule{Efq} rule, that we included for that very purpose,
 that is, to skip non-selectable branches during typing. The choice of one
 or the other approach is mostly a matter of taste and, in this specific case,
 boils down to deciding whether some typing problems must be
@@ -111,7 +111,7 @@ negated arrows, the only purpose of this extension being to prove type preservat
 to, not only because we favor type preserving systems, but also
 because in this way we were able to characterize different subsystems that
 are complete with respect to the algorithmic system, thus exploring
-different language design and arguing about the usefulness.
+different language designs and arguing about their usefulness.
 }%%%rev
 
 Another direction of research related to ours is the one of semantic