Index: doc/aaron_comp_II/comp_II.tex
===================================================================
--- doc/aaron_comp_II/comp_II.tex	(revision d5905a2d7013853629079394e55a4a428e625a5f)
+++ doc/aaron_comp_II/comp_II.tex	(revision ff3fc936860505713ed81ebb530f81e2656a37d0)
@@ -85,9 +85,10 @@
 
 \CFA\footnote{Pronounced ``C-for-all'', and written \CFA, CFA, or \CFL.} is an evolutionary modernization of the C programming language currently being designed and built at the University of Waterloo by a team led by Peter Buhr. 
-Features added to C by \CFA include name overloading, user-defined operators, parametric-polymorphic routines, and type constructors and destructors, among others. 
-These features make \CFA significantly more powerful and expressive than C, but impose a significant compile-time cost to implement, particularly in the expression resolver, which must evaluate the typing rules of a much more complex type system. 
+\CFA adds multiple features to C, including name overloading, user-defined operators, parametric-polymorphic routines, and type constructors and destructors, among others. 
+These features make \CFA significantly more powerful and expressive than C, but impose a significant compile-time cost to support, particularly in the expression resolver, which must evaluate the typing rules of a much more complex type system. 
 The primary goal of this proposed research project is to develop a sufficiently performant expression resolution algorithm, experimentally validate its performance, and integrate it into \Index*{CFA-CC}, the \CFA reference compiler.
 Secondary goals of this project include the development of various new language features for \CFA; parametric-polymorphic (``generic'') types have already been designed and implemented, and reference types and user-defined conversions are under design consideration. 
-The experimental performance-testing architecture for resolution algorithms will also be used to determine the compile-time cost of adding such new features to the \CFA type system.
+The experimental performance-testing architecture for resolution algorithms will also be used to determine the compile-time cost of adding such new features to the \CFA type system. 
+More broadly, this research should provide valuable data for implementers of compilers for other programming languages with similarly powerful static type systems.
 
 \section{\CFA}
@@ -98,5 +99,5 @@
 \subsection{Polymorphic Functions}
 The most significant feature \CFA adds is parametric-polymorphic functions. 
-Such functions are written using a ©forall© clause, the feature that gave the language its name:
+Such functions are written using a ©forall© clause (which gives the language its name):
 \begin{lstlisting}
 forall(otype T)
@@ -126,5 +127,5 @@
 
 Monomorphic specializations of polymorphic functions can themselves be used to satisfy type assertions. 
-For instance, ©twice© could have been define as below, using the \CFA syntax for operator overloading:
+For instance, ©twice© could have been defined as below, using the \CFA syntax for operator overloading:
 \begin{lstlisting}
 forall(otype S | { S ?+?(S, S); })
@@ -132,10 +133,10 @@
 \end{lstlisting} 
 This version of ©twice© will work for any type ©S© that has an addition operator defined for it, and it could have been used to satisfy the type assertion on ©four_times©. 
-The compiler accomplishes this by creating a wrapper function calling ©twice // (2)© with ©S© bound to ©double©, then providing this wrapper function to ©four_times©\footnote{©twice // (2)© could have had a type parameter named ©T©; \CFA specifies a renaming the type parameters, which would avoid the name conflict with the parameter ©T© of ©four_times©.}. 
+The compiler accomplishes this by creating a wrapper function calling ©twice // (2)© with ©S© bound to ©double©, then providing this wrapper function to ©four_times©\footnote{©twice // (2)© could also have had a type parameter named ©T©; \CFA specifies renaming of the type parameters, which would avoid the name conflict with the type variable ©T© of ©four_times©.}. 
 
 Finding appropriate functions to satisfy type assertions is essentially a recursive case of expression resolution, as it takes a name (that of the type assertion) and attempts to match it to a suitable declaration in the current scope. 
 If a polymorphic function can be used to satisfy one of its own type assertions, this recursion may not terminate, as it is possible that function will be examined as a candidate for its own type assertion unboundedly repeatedly. 
 To avoid infinite loops, the current \Index*{CFA-CC} compiler imposes a fixed limit on the possible depth of recursion, similar to that employed by most \Index*[C++]{\CC} compilers for template expansion; this restriction means that there are some semantically well-typed expressions which cannot be resolved by {CFA-CC}. 
-One area of potential improvement this project proposes to investigate is the possibility of using the compiler's knowledge of the current set of declarations to make a more precise judgement of when further type assertion satisfaction recursion will not produce a well-typed expression.
+One area of potential improvement this project proposes to investigate is the possibility of using the compiler's knowledge of the current set of declarations to more precicely determine when further type assertion satisfaction recursion will not produce a well-typed expression.
 
 \subsection{Name Overloading}
@@ -168,5 +169,5 @@
 Such a conversion system should be simple for user programmers to utilize, and fit naturally with the existing design of implicit conversions in C; ideally it would also be sufficiently powerful to encode C's usual arithmetic conversions itself, so that \CFA only has one set of rules for conversions. 
 
-Glen Ditchfield \textbf{TODO CITE} has laid out a framework for using polymorphic conversion constructor functions to create a directed acyclic graph (DAG) of conversions. 
+Ditchfield\cite{Ditchfield:conversions} has laid out a framework for using polymorphic conversion constructor functions to create a directed acyclic graph (DAG) of conversions. 
 A monomorphic variant of these functions can be used to mark a conversion arc in the DAG as only usable as the final step in a conversion. 
 With these two types of conversion arcs, separate DAGs can be created for the safe and the unsafe conversions, and conversion cost can be represented as path length through the DAG. 
@@ -207,5 +208,5 @@
 \CFA adds \emph{tuple types} to C, a facility for referring to multiple values with a single identifier. 
 A variable may name a tuple, and a function may return one. 
-Particularly relevantly for resolution, a tuple may be automatically \emph{destructured} into a list of values, as in the ©swap© function below:
+Particularly relevantly for resolution, a tuple may be implicitly \emph{destructured} into a list of values, as in the call to ©swap© below:
 \begin{lstlisting}
 [char, char] x = [ '!', '?' ];
@@ -215,5 +216,5 @@
 
 x = swap( x ); // destructure [char, char] x into two elements of parameter list
-// ^ can't use int x for parameter, not enough arguments to swap
+// can't use int x for parameter, not enough arguments to swap
 \end{lstlisting}
 Tuple destructuring means that the mapping from the position of a subexpression in the argument list to the position of a paramter in the function declaration is not straightforward, as some arguments may be expandable to different numbers of parameters, like ©x© above.
@@ -250,10 +251,11 @@
 
 The research goal of this project is to develop a performant expression resolver for \CFA; this analysis suggests two primary areas of investigation to accomplish that end. 
-The first is efficient argument-parameter matching; Bilson\cite{Bilson03} mentions significant optimization opportunities available in the current literature to improve on the existing {CFA-CC} compiler \textbf{TODO:} \textit{look up and lit review}. 
+The first is efficient argument-parameter matching; Bilson\cite{Bilson03} mentions significant optimization opportunities available in the current literature to improve on the existing {CFA-CC} compiler.
+%TODO: look up and lit review 
 The second, and likely more fruitful, area of investigation is heuristics and algorithmic approaches to reduce the number of argument interpretations considered in the common case; given the large ($p+1$) exponent on number of interpretations considered in the runtime analysis, even small reductions here could have a significant effect on overall resolver runtime. 
 The discussion below presents a number of largely orthagonal axes for expression resolution algorithm design to be investigated, noting prior work where applicable. 
 
 \subsection{Argument-Parameter Matching}
-The first axis we consider is argument-parameter matching - whether the type matching for a candidate function to a set of candidate arguments is directed by the argument types or the parameter types. 
+The first axis we consider is argument-parameter matching --- whether the type matching for a candidate function to a set of candidate arguments is directed by the argument types or the parameter types. 
 
 \subsubsection{Argument-directed (``Bottom-up'')}
@@ -296,5 +298,5 @@
 \subsubsection{On Arguments}
 Another approach would be to generate a set of possible implicit conversions for each set of interpretations of a given argument. 
-This would have the benefit of detecting ambiguous interpretations of arguments at the level of the argument rather than its containing call, and would also never find more than one interpretation of the argument with a given type. 
+This would have the benefit of detecting ambiguous interpretations of arguments at the level of the argument rather than its containing call, would also never find more than one interpretation of the argument with a given type, and would re-use calculation of implicit conversions between function candidates. 
 On the other hand, this approach may unncessarily generate argument interpretations that will never match a parameter, wasting work.
 
@@ -321,5 +323,5 @@
 Under this approach the \CFA resolver could, for instance, try expression interpretations in the following order:
 \begin{enumerate}
-\item All interpretations with no polymorphic type binding or implicit conversions.
+\item Interpretations with no polymorphic type binding or implicit conversions.
 \item Interpretations containing no polymorphic type binding and at least one safe implicit conversion.
 \item Interpretations containing polymorphic type binding, but only safe implicit conversions.
@@ -370,4 +372,6 @@
 The experimental results will also provide some empirical sense of the compile-time cost of various language features by comparing the results of the most performant resolver variant that supports the feature with the most performant resolver variant that doesn't, a useful capability to guide language design.
 
+This proposed project should provide valuable data on how to implement a performant compiler for modern programming languages such as \CFA with powerful static type systems, specifically targeting the feature interaction between name overloading and implicit conversions.
+
 \appendix
 \section{Completion Timeline}
Index: doc/bibliography/cfa.bib
===================================================================
--- doc/bibliography/cfa.bib	(revision d5905a2d7013853629079394e55a4a428e625a5f)
+++ doc/bibliography/cfa.bib	(revision ff3fc936860505713ed81ebb530f81e2656a37d0)
@@ -1623,4 +1623,15 @@
     year	= 1974,
 }
+
+@unpublished{Ditchfield:conversions,
+	contributer = {a3moss@uwaterloo.ca},
+	author = {Glen Ditchfield},
+	title = {Conversions for {Cforall}},
+	note = {\href{http://plg.uwaterloo.ca/~cforall/Conversions/index.html}{http://\-plg.uwaterloo.ca/\-\textasciitilde cforall/\-Conversions/\-index.html}},
+	month = {Nov},
+	year = {2002},
+	urldate = {28 July 2016},
+}
+
 
 @techreport{Dijkstra65,
