Index: doc/bibliography/cfa.bib
===================================================================
--- doc/bibliography/cfa.bib	(revision c13b2b8eef2cfbfbdaad72b466afc688f532f9e4)
+++ doc/bibliography/cfa.bib	(revision 2ca35b110e276c9f4e3132f8fe17bfabf0a643ed)
@@ -6221,4 +6221,17 @@
 }
 
+@article{Smith98,
+  keywords = {Polymorphic C},
+  contributor = {a3moss@uwaterloo.ca},
+  title={A sound polymorphic type system for a dialect of C},
+  author={Smith, Geoffrey and Volpano, Dennis},
+  journal={Science of computer programming},
+  volume={32},
+  number={1-3},
+  pages={49--72},
+  year={1998},
+  publisher={Elsevier}
+}
+
 @book{Campbell74,
     keywords	= {path expressions},
Index: doc/generic_types/generic_types.tex
===================================================================
--- doc/generic_types/generic_types.tex	(revision c13b2b8eef2cfbfbdaad72b466afc688f532f9e4)
+++ doc/generic_types/generic_types.tex	(revision 2ca35b110e276c9f4e3132f8fe17bfabf0a643ed)
@@ -1023,6 +1023,5 @@
 \section{Related Work}
 
-
-\subsection{Polymorphism}
+% \subsection{Polymorphism}
 
 \CC is the most similar language to \CFA;
@@ -1034,5 +1033,5 @@
 In contrast, \CFA has a single facility for polymorphic code supporting type-safe separate-compilation of polymorphic functions and generic (opaque) types, which uniformly leverage the C procedural paradigm.
 The key mechanism to support separate compilation is \CFA's \emph{explicit} use of assumed properties for a type.
-Until \CC~\citep{C++Concepts} are standardized (anticipated for \CCtwenty), \CC provides no way to specify the requirements of a generic function in code beyond compilation errors during template expansion;
+Until \CC~\citet{C++Concepts} are standardized (anticipated for \CCtwenty), \CC provides no way to specify the requirements of a generic function in code beyond compilation errors during template expansion;
 furthermore, \CC concepts are restricted to template polymorphism.
 
@@ -1042,13 +1041,13 @@
 In \CFA terms, all Cyclone polymorphism must be dtype-static.
 While the Cyclone design provides the efficiency benefits discussed in Section~\ref{sec:generic-apps} for dtype-static polymorphism, it is more restrictive than \CFA's general model.
+\citet{Smith98} present Polymorphic C, an ML dialect with polymorphic functions and C-like syntax and pointer types; it lacks many of C's features, however, most notably struct types, and so is not a practical C replacement.
 
 \citet{obj-c-book} is an industrially successful extension to C.
 However, Objective-C is a radical departure from C, using an object-oriented model with message-passing.
-Objective-C did not support type-checked generics until recently~\citet{xcode7}, historically using less-efficient and more error-prone runtime checking of object types.
+Objective-C did not support type-checked generics until recently \citep{xcode7}, historically using less-efficient runtime checking of object types.
 The~\citet{GObject} framework also adds object-oriented programming with runtime type-checking and reference-counting garbage-collection to C;
 these features are more intrusive additions than those provided by \CFA, in addition to the runtime overhead of reference-counting.
-\citet{Vala} compiles to GObject-based C, and so adds the burden of learning a separate language syntax to the aforementioned demerits of GObject as a modernization path for the existing C code-bases.
-Java~\citep{Java8} included generic types in Java~5;
-Java's generic types are type-checked at compilation and type-erased at runtime, similar to \CFA's.
+\citet{Vala} compiles to GObject-based C, adding the burden of learning a separate language syntax to the aforementioned demerits of GObject as a modernization path for existing C code-bases.
+Java~\citep{Java8} included generic types in Java~5 which are type-checked at compilation and type-erased at runtime, similar to \CFA's.
 However, in Java, each object carries its own table of method pointers, while \CFA passes the method pointers separately to maintain a C-compatible layout.
 Java is also a garbage-collected, object-oriented language, with the associated resource usage and C-interoperability burdens.
@@ -1064,6 +1063,5 @@
 \CFA, with its more modest safety features, allows direct ports of C code while maintaining the idiomatic style of the original source.
 
-
-\subsection{Tuples/Variadics}
+% \subsection{Tuples/Variadics}
 
 Many programming languages have some form of tuple construct and/or variadic functions, \eg SETL, C, KW-C, \CC, D, Go, Java, ML, and Scala.
@@ -1098,9 +1096,9 @@
 
 There is ongoing work on a wide range of \CFA feature extensions, including reference types, exceptions, concurrent primitives and modules.
-(While all examples in the paper compile and run, a public beta-release of \CFA will take another 8--12 months to finalize these addition extensions.)
+(While all examples in the paper compile and run, a public beta-release of \CFA will take another 8--12 months to finalize these additional extensions.)
 In addition, there are interesting future directions for the polymorphism design.
 Notably, \CC template functions trade compile time and code bloat for optimal runtime of individual instantiations of polymorphic functions.
-\CFA polymorphic functions uses a dynamic virtual-dispatch.
-The runtime overhead of this approach is low, but not as low as inlining, and it may be beneficial to provide a mechanism for performance-sensitive code.
+\CFA polymorphic functions use dynamic virtual-dispatch; 
+the runtime overhead of this approach is low, but not as low as inlining, and it may be beneficial to provide a mechanism for performance-sensitive code.
 Two promising approaches are an @inline@ annotation at polymorphic function call sites to create a template-specialization of the function (provided the code is visible) or placing an @inline@ annotation on polymorphic function-definitions to instantiate a specialized version for some set of types.
 These approaches are not mutually exclusive and allow performance optimizations to be applied only when necessary, without suffering global code-bloat.
