Index: doc/theses/aaron_moss_PhD/phd/introduction.tex
===================================================================
--- doc/theses/aaron_moss_PhD/phd/introduction.tex	(revision 39de1c5509618f7fa261127870a0d93070f254fa)
+++ doc/theses/aaron_moss_PhD/phd/introduction.tex	(revision 69c37ccfbd57ffcac000650a919c9708faf8c701)
@@ -39,5 +39,5 @@
 \cbstart
 The prototype system, which implements the algorithmic contributions of this thesis, is the first performant type-checker implementation for a \CFA{}-style type system. 
-As the existence of an efficient compiler is necessary for the practical viability of a programming language, the contributions of this thesis comprise a validation of the \CFA{} language design which was previously lacking.
+As the existence of an efficient compiler is necessary for the practical viability of a programming language, the contributions of this thesis comprise a validation of the \CFA{} language design that was previously lacking.
 \cbend
 
@@ -45,17 +45,17 @@
 In particular, with the addition of \emph{concepts} in \CCtwenty{}~\cite{C++Concepts}, conforming \CC{} compilers must support a model of type assertions very similar to that in \CFA{}, and the algorithmic techniques used here may prove useful. 
 \cbstart
-Much of the difficulty of type-checking \CFA{} stems from the language design choice to allow type inference from the context of a function call in addition to its arguments; this feature allows the programmers to specify fewer redundant type annotations on functions which are polymorphic in their return type.
+Much of the difficulty of type-checking \CFA{} stems from the language design choice to allow type inference from the context of a function call in addition to its arguments; this feature allows the programmers to specify fewer redundant type annotations on functions that are polymorphic in their return type.
 \cbend \cbstartx
 The !auto! keyword in \CCeleven{} supports a similar but sharply restricted form of this contextual inference -- the demonstration of the richer inference in \CFA{} raises possibilities for similar features in future versions of \CC{}. 
 By contrast, Java~8~\cite{Java8} and Scala~\cite{Scala} use comparably powerful forms of type inference, so the algorithmic techniques in this thesis may be effective for those languages' compiler implementors. 
 \cbendx
-Type environments are also widely modelled in compiler implementations, particularly for functional languages, though also increasingly commonly for other languages (such as Rust~\cite{Rust}) which perform type inference; the type environment presented here may be useful to those language implementors.
+Type environments are also widely modelled in compiler implementations, particularly for functional languages, though also increasingly commonly for other languages (such as Rust~\cite{Rust}) that perform type inference; the type environment presented here may be useful to those language implementors.
 
 \cbstarty
-One area of inquiry which is outside the scope of this thesis is formalization of the \CFA{} type system. 
+One area of inquiry that is outside the scope of this thesis is formalization of the \CFA{} type system. 
 Ditchfield~\cite{Ditchfield92} defined the $F_\omega^\ni$ polymorphic lambda calculus which is the theoretical basis for the \CFA{} type system. 
 Ditchfield did not, however, prove any soundness or completeness properties for $F_\omega^\ni$; such proofs remain future work. 
 A number of formalisms other than $F_\omega^\ni$ could potentially be adapted to model \CFA{}. 
-One promising candidate is \emph{local type inference} \cite{Pierce00,Odersky01}, which describes similar contextual propagation of type information; another is the polymorphic conformity-based model of the Emerald~\cite{Black90} programming language, which defines a subtyping relation on types which are conceptually similar to \CFA{} traits.
+One promising candidate is \emph{local type inference} \cite{Pierce00,Odersky01}, which describes similar contextual propagation of type information; another is the polymorphic conformity-based model of the Emerald~\cite{Black90} programming language, which defines a subtyping relation on types that are conceptually similar to \CFA{} traits.
 These modelling approaches could potentially be used to extend an existing formal semantics for C such as Cholera \cite{Norrish98}, CompCert \cite{Leroy09}, or Formalin \cite{Krebbers14}.
 \cbendy
