Index: doc/bibliography/pl.bib
===================================================================
--- doc/bibliography/pl.bib	(revision 71a12390eb03a6fdd2beefb60f5a0838f37b2ea8)
+++ doc/bibliography/pl.bib	(revision ec92b486dc79c3f86a026bcb1454ad883b592f39)
@@ -1148,4 +1148,11 @@
     year	= 1998,
     note	= {{\small\textsf{ftp://\-plg.uwaterloo.ca/\-pub/\-Cforall/\-refrat.ps.gz}}},
+}
+
+@phdthesis{Norrish98,
+  title={C formalised in HOL},
+  author={Norrish, Michael},
+  year={1998},
+  school={University of Cambridge}
 }
 
@@ -3154,4 +3161,25 @@
     year	= 2018,
 }
+
+@article{Leroy09,
+ keywords = {C formalization},
+ contributer = {a3moss@uwaterloo.ca},
+ author = {Leroy, Xavier},
+ title = {Formal Verification of a Realistic Compiler},
+ journal = {Commun. ACM},
+ issue_date = {July 2009},
+ volume = {52},
+ number = {7},
+ month = jul,
+ year = {2009},
+ issn = {0001-0782},
+ pages = {107--115},
+ numpages = {9},
+ url = {http://doi.acm.org/10.1145/1538788.1538814},
+ doi = {10.1145/1538788.1538814},
+ acmid = {1538814},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+} 
 
 @manual{Fortran95,
@@ -5316,4 +5344,23 @@
 }
 
+@inproceedings{Krebbers14,
+ keywords = {c formalization},
+ contributer = {a3moss@uwaterloo.ca},
+ author = {Krebbers, Robbert},
+ title = {An Operational and Axiomatic Semantics for Non-determinism and Sequence Points in C},
+ booktitle = {Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
+ series = {POPL '14},
+ year = {2014},
+ isbn = {978-1-4503-2544-8},
+ location = {San Diego, California, USA},
+ pages = {101--112},
+ numpages = {12},
+ url = {http://doi.acm.org/10.1145/2535838.2535878},
+ doi = {10.1145/2535838.2535878},
+ acmid = {2535878},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+} 
+
 @book{Deitel04,
     keywords	= {concurrency, operating systems},
@@ -7612,4 +7659,11 @@
 }
 
+@techreport{Black90,
+  title={Typechecking polymorphism in {Emerald}},
+  author={Black, Andrew P and Hutchinson, Norman C},
+  year={1990},
+  institution={Cambridge Research Laboratory, Digital Equipment Corporation}
+}
+
 @article{Cormack90,
     keywords	= {polymorphism},
Index: doc/theses/aaron_moss_PhD/phd/background.tex
===================================================================
--- doc/theses/aaron_moss_PhD/phd/background.tex	(revision 71a12390eb03a6fdd2beefb60f5a0838f37b2ea8)
+++ doc/theses/aaron_moss_PhD/phd/background.tex	(revision ec92b486dc79c3f86a026bcb1454ad883b592f39)
@@ -379,2 +379,11 @@
 \CFA{} adds a significant number of features to standard C, increasing the expressivity and re-usability of \CFA{} code while maintaining backwards compatibility for both code and larger language paradigms. 
 This flexibility does incur significant added compilation costs, however, the mitigation of which are the primary concern of this thesis.
+
+\cbstarty
+One area of inquiry which 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.
+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
Index: doc/theses/aaron_moss_PhD/phd/thesis.tex
===================================================================
--- doc/theses/aaron_moss_PhD/phd/thesis.tex	(revision 71a12390eb03a6fdd2beefb60f5a0838f37b2ea8)
+++ doc/theses/aaron_moss_PhD/phd/thesis.tex	(revision ec92b486dc79c3f86a026bcb1454ad883b592f39)
@@ -36,4 +36,6 @@
 \newcommand{\cbstartx}{\cbcolor{red} \cbstart}
 \newcommand{\cbendx}{\cbend \cbcolor{blue}}
+\newcommand{\cbstarty}{\cbcolor{green} \cbstart}
+\newcommand{\cbendy}{\cbend \cbcolor{blue}}
 
 % Hyperlinks make it very easy to navigate an electronic document.