Index: doc/bibliography/pl.bib
===================================================================
--- doc/bibliography/pl.bib	(revision 9a38436cacd273d6f50f58a7a3f9bd7013e825a9)
+++ doc/bibliography/pl.bib	(revision f2c5726d5f2802d935e7a45e12307d1026459024)
@@ -4175,4 +4175,17 @@
 }
 
+@misc{Haberman16,
+    keywords	= {C++ template expansion},
+    contributer	= {a3moss@uwaterloo.ca},
+    author	= {Josh Haberman},
+    title	= {Making arbitrarily-large binaries from fixed-size {C}{\kern-.1em\hbox{\large\texttt{+\kern-.25em+}}} code},
+    year	= 2016,
+    howpublished= {\href{http://blog.reverberate.org/2016/01/making-arbitrarily-large-binaries-from.html}
+		  {
+          {http://blog.reverberate.org/\-2016/\-01/\-making-arbitrarily-large-binaries-from.html}
+          }},
+    optnote	= {Accessed: 2016-09},
+}
+
 @article{c++libs,
     keywords	= {directory structure},
Index: doc/theses/aaron_moss_PhD/phd/resolution-heuristics.tex
===================================================================
--- doc/theses/aaron_moss_PhD/phd/resolution-heuristics.tex	(revision 9a38436cacd273d6f50f58a7a3f9bd7013e825a9)
+++ doc/theses/aaron_moss_PhD/phd/resolution-heuristics.tex	(revision f2c5726d5f2802d935e7a45e12307d1026459024)
@@ -1,4 +1,6 @@
 \chapter{Resolution Heuristics}
 \label{resolution-chap}
+
+% consider using "satisfaction" throughout when talking about assertions
 
 The main task of the \CFACC{} type-checker is \emph{expression resolution}, determining which declarations the identifiers in each expression correspond to. 
@@ -138,4 +140,29 @@
 \section{Resolution Algorithms}
 
+\CFA{} expression resolution is not, in general, polynomial in the size of the input expression, as shown in Section~\ref{resn-analysis-sec}. 
+While this theoretical result is daunting, its implications can be mitigated in practice.
+\CFACC{} does not solve one instance of expression resolution in the course of compiling a program, but rather thousands; therefore, if the worst case of expression resolution is sufficiently rare, worst-case instances can be amortized by more-common easy instances for an acceptable overall runtime. 
+Secondly, while a programmer \emph{can} deliberately generate a program designed for inefficient compilation\footnote{see for instance \cite{Haberman16}, which generates arbitrarily large \CC{} template expansions from a fixed-size source file.}, source code tends to follow common patterns. 
+Programmers generally do not want to run the full compiler algorithm in their heads, and as such keep mental shortcuts in the form of language idioms. 
+If the compiler can be tuned to handle idiomatic code more efficiently, then the reduction in runtime for idiomatic (but otherwise difficult) resolution instances can make a significant difference in total compiler runtime. 
+
+\subsection{Analysis} \label{resn-analysis-sec}
+
+Expression resolution has a number of components which contribute to its runtime, including argument-parameter type unification, recursive traversal of the expression tree, and satisfaction of type assertions. 
+
+If the bound type for a type variable can be looked up or mutated in constant time (as asserted in Table~\ref{env-bounds-table}), then the runtime of the unification algorithm to match an argument to a parameter is proportional to the complexity of the types being unified. 
+In C, complexity of type representation is bounded by the most-complex type explicitly written in a declaration; in \CFA{}, however, polymorphism can generate more-complex types: 
+
+\begin{cfa}
+	forall(otype T) pair(T) wrap(T x, T y);
+
+	wrap(wrap(wrap(1, 2), wrap(3, 4)), wrap(wrap(5, 6), wrap(7, 8)));
+\end{cfa}
+
+To resolve the outermost !wrap!, the resolver must check that !pair(pair(int))! unifies with itself, but at three levels of nesting, !pair(pair(int))! is more complex than either !pair(T)! or !T!, the types in the declaration of !wrap!. 
+According to this argument, then, the cost of a single argument-parameter unification is !O(d)!, where !d! is the depth of the expression tree, and the cost of argument-parameter unification for a single candidate for a given function call expression is !O(pd)!, where !p! is the number of parameters. 
+
+% continue from here
+
 \subsection{Related Work}
 
@@ -147,4 +174,12 @@
 I have modified \CFACC{} to first sort assertion satisfaction candidates by conversion cost, and only resolve recursive assertions until a unique minimal-cost candidate or an ambiguity is detected.
 
+\section{Experimental Results}
+
+% use Jenkins daily build logs to rebuild speedup graph with more data
+
+% look back at Resolution Algorithms section for threads to tie up "does the algorithm look like this?"
+
+\section{Conclusion \& Future Work}
+
 I have experimented with using expression resolution rather than type unification to choose assertion resolutions; this path should be investigated further in future work. 
 This approach is more flexible than type unification, allowing for conversions to be applied to functions to satisfy assertions. 
@@ -153,3 +188,5 @@
 The main challenge to implement this approach in \CFACC{} would be applying the implicit conversions generated by the resolution process in the code-generation for the thunk functions that \CFACC{} uses to pass type assertions with the proper signatures.
 
+% Discuss possibility of parallel subexpression resolution
+
 % Mention relevance of work to C++20 concepts