Index: doc/theses/aaron_moss_PhD/phd/Makefile
===================================================================
--- doc/theses/aaron_moss_PhD/phd/Makefile	(revision 21cf1018c214e9fe47acd9521e6f5a80206445e7)
+++ doc/theses/aaron_moss_PhD/phd/Makefile	(revision 0e6a0bebb41b45cf615f928ea49e1295870c1fc7)
@@ -23,6 +23,7 @@
 background \
 generic-types \
+resolution-heuristics \
 type-environment \
-resolution-heuristics \
+experiments \
 conclusion \
 }
Index: doc/theses/aaron_moss_PhD/phd/background.tex
===================================================================
--- doc/theses/aaron_moss_PhD/phd/background.tex	(revision 21cf1018c214e9fe47acd9521e6f5a80206445e7)
+++ doc/theses/aaron_moss_PhD/phd/background.tex	(revision 0e6a0bebb41b45cf615f928ea49e1295870c1fc7)
@@ -1,3 +1,4 @@
 \chapter{\CFA{}}
+\label{cfa-chap}
 
 \CFA{} adds a number of features to C, some of them providing significant increases to the expressive power of the language, but all designed to maintain the existing procedural programming paradigm of C and to be as orthogonal as possible to each other. 
Index: doc/theses/aaron_moss_PhD/phd/experiments.tex
===================================================================
--- doc/theses/aaron_moss_PhD/phd/experiments.tex	(revision 0e6a0bebb41b45cf615f928ea49e1295870c1fc7)
+++ doc/theses/aaron_moss_PhD/phd/experiments.tex	(revision 0e6a0bebb41b45cf615f928ea49e1295870c1fc7)
@@ -0,0 +1,58 @@
+\chapter{Experiments}
+\label{expr-chap}
+
+I have implemented a prototype system to test the practical effectiveness of the various algorithms described in Chapters~\ref{resolution-chap} and~\ref{env-chap}. 
+This prototype system essentially just implements the expression resolution pass of \CFACC{}, with a simplified version of the \CFA{} type system and a parser to read in problem instances. 
+The prototype system allows for quicker iteration on algorithms due to its simpler language model and lack of a requirement to generate runnable code, yet captures enough of the nuances of \CFA{} to have some predictive power for the runtime performance of algorithmic variants in \CFACC{} itself. 
+
+There are three sources of problem instances for the resolver prototype. 
+The first is small, hand-written tests designed to test the expressive power and correctness of the prototype. 
+These tests are valuable for regression testing, but not time-consuming enough to be useful performance tests. 
+The second sort of problem instances are procedurally generated according to a set of parameters (\eg{} distributions of polymorphic versus monomorphic functions, number of function arguments, number of types, \etc{}); the procedural problem generator can be used to explore the behaviour of an algorithm with respect to certain sorts of problem instances by varying the input parameters. 
+I have implemented a flagged \CFACC{} pass which outputs information which can be used to initialize the procedural generator's parameters to realistic values. 
+The final sort of problem instances are derived from actual \CFA{} code. 
+The prototype has a rich enough representation of \CFA{} that actual instances of expression resolution can be expressed with good fidelity, and I have implemented a compiler pass for \CFACC{} which can generate instances from actual code. 
+Since at this juncture all development in \CFA{} is done by our research team, I have tested the prototype system on all \CFA{} code currently extant, primarily the standard library and compiler test suite.
+
+\section{Resolver Prototype Features}
+
+The resolver prototype can express most of the \CFA{} features described in Chapter~\ref{cfa-chap}. 
+It supports both monomorphic and polymorphic functions, with type assertions for polymorphic functions. 
+Traits are not explicitly represented, but \CFACC{} inlines traits before the resolver pass, so this is a faithful representation of the existing compiler problem. 
+The prototype system supports variable declarations as well as function declarations, and has a lexical-scoping scheme which obeys \CFA{}-like overloading and overriding rules. 
+
+The type system of the resolver prototype also captures the key aspects of the \CFA{} type system. 
+\emph{Concrete types} represent the built-in arithmetic types of \CFA{}, along with the implicit conversions between them. 
+Each concrete type is represented by an integer ID, and the conversion cost from $x$ to $y$ is $|y-x|$, a safe conversion if $y > x$, or an unsafe conversion if $y < x$. 
+This is markedly simpler than the graph of conversion costs in \CFA{}, but captures the essentials of the design well. 
+For simplicity, !zero_t! and !one_t!, the types of !0! and !1!, are represented by the type corresponding to !int!.
+\emph{Named types} are analogues to \CFA{} aggregates, such as structs and unions; aggregate fields are encoded as unary functions from the struct type to the field type, named based on the field name. 
+Named types also support type parameters, and as such can represent generic types as well. 
+Generic named types are used to represent the built-in parameterized types of \CFA{} as well; !T*! is encoded as \texttt{\#\$ptr<T>}. 
+\CFA{} arrays are also represented as pointers, to simulate array-to-pointer decay, while top-level reference types are replaced by their referent to simulate the variety of reference conversions. 
+Function types have first-class representation in the prototype as the type of both function declarations and function pointers, though the function type in the prototype system loses information about type assertions, so polymorphic function pointers cannot be expressed.
+Void and tuple types are also supported in the prototype, to express the multiple-return-value functions in \CFA{}, though varargs functions and !ttype! tuple-typed type variables are absent from the prototype system.
+The prototype system also does not represent type qualifiers (\eg{} !const!, !volatile!), so all such qualifiers are stripped during conversion to the prototype system. 
+
+The resolver prototype supports three sorts of expressions in its input language. 
+The simplest are \emph{value expressions}, which are expressions declared to be a certain type; these implement literal expressions in \CFA{}, and, already being typed, are passed through the resolver unchanged.
+The second sort, \emph{name expressions}, represent a variable expression in \CFA{}; these contain the name of a variable or function, and are matched to an appropriate declaration overloading that name by the resolver. 
+The third input expression, the \emph{function expression}, represents a call to a function, with a name and zero or more argument subexpressions. 
+As is usual in \CFA{}, operators are represented as function calls; however, as mentioned above, the prototype system represents field access expressions !a.f! as function expressions as well. 
+
+The main area for future expansion in the design of the resolver prototype is conversions. 
+Cast expressions are implemented in the output language of the resolver, but cannot be expressed in the input. 
+The only implicit conversions supported are between the arithmetic-like concrete types, which captures most, but not all, of \CFA{}'s built-in implicit conversions\footnote{Notable absences include \lstinline{void*} to other pointer types, or \lstinline{0} to pointer types.}. 
+Future work should include a way to express implicit (and possibly explicit) conversions in the input language, with an investigation of the most efficient way to handle implicit conversions, and potentially design for user-defined conversions.
+
+\section{Resolver Prototype Design}
+
+% talk about GC here, associated visitor/AST design
+
+% talk about shared type representations
+
+\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?"
Index: doc/theses/aaron_moss_PhD/phd/resolution-heuristics.tex
===================================================================
--- doc/theses/aaron_moss_PhD/phd/resolution-heuristics.tex	(revision 21cf1018c214e9fe47acd9521e6f5a80206445e7)
+++ doc/theses/aaron_moss_PhD/phd/resolution-heuristics.tex	(revision 0e6a0bebb41b45cf615f928ea49e1295870c1fc7)
@@ -293,5 +293,5 @@
 If the assertions of the minimal-cost top-level interpretation cannot be satisfied then the next-most-minimal-cost interpretation's assertions are checked, and so forth until a minimal-cost satisfiable interpretation (or ambiguous set thereof) is found, or no top-level interpretations are found to have satisfiable assertions. 
 In the common case where the code actually does compile this saves the work of checking assertions for ultimately-rejected interpretations, though it does rule out some pruning opportunities for subinterpretations with unsatisfiable assertions or which are more expensive than a minimal-cost polymorphic function with the same return type. 
-The experimental results in Section~\ref{resn-expr-sec} indicate that this is a worthwhile trade-off. 
+The experimental results in Chapter~\ref{expr-chap} indicate that this is a worthwhile trade-off. 
 
 Optimizing assertion satisfaction for common idioms has also proved effective in \CFA{}; the code below is an unexceptional print statement derived from the \CFA{} test suite that nonetheless is a very difficult instance of expression resolution:
@@ -326,10 +326,4 @@
 As such, I opted to continue Bilson's approach of designing a bespoke solver for \CFA{} assertion satisfaction, rather than attempting to re-express the problem in some more general formalism. 
 
-\section{Experimental Results} \label{resn-expr-sec}
-
-% 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}
 
Index: doc/theses/aaron_moss_PhD/phd/thesis.tex
===================================================================
--- doc/theses/aaron_moss_PhD/phd/thesis.tex	(revision 21cf1018c214e9fe47acd9521e6f5a80206445e7)
+++ doc/theses/aaron_moss_PhD/phd/thesis.tex	(revision 0e6a0bebb41b45cf615f928ea49e1295870c1fc7)
@@ -132,4 +132,5 @@
 \input{resolution-heuristics}
 \input{type-environment}
+\input{experiments}
 \input{conclusion}
 
Index: doc/theses/aaron_moss_PhD/phd/type-environment.tex
===================================================================
--- doc/theses/aaron_moss_PhD/phd/type-environment.tex	(revision 21cf1018c214e9fe47acd9521e6f5a80206445e7)
+++ doc/theses/aaron_moss_PhD/phd/type-environment.tex	(revision 0e6a0bebb41b45cf615f928ea49e1295870c1fc7)
@@ -265,5 +265,3 @@
 Persistent union-find, as the name suggests, is more optimized, with $O(1)$ cost to $save$ a backtrack-capable reference to the current environment state, and $O(p)$ cost to revert to that state (possibly destroying no-longer-used edit nodes along the path).
 
-\section{Experiments}
-
 % Future work: design multi-threaded version of C&F persistent map --- core idea is some sort of thread-boundary edit node
