Index: doc/theses/jiada_liang_MMath/CEnum.tex
===================================================================
--- doc/theses/jiada_liang_MMath/CEnum.tex	(revision af5baae0adea725769db51743818a97dfe619952)
+++ doc/theses/jiada_liang_MMath/CEnum.tex	(revision 0c51c8b42a007627bcf2537dfce73151c5a015ef)
@@ -7,6 +7,6 @@
 
 
-\section{Enumerator Visibility}
-\label{s:EnumeratorVisibility}
+\section{Visibility}
+\label{s:CVisibility}
 
 In C, unscoped enumerators present a \newterm{naming problem} when multiple enumeration types appear in the same scope with duplicate enumerator names.
@@ -42,5 +42,5 @@
 
 
-\section{Enumerator Scoping}
+\section{Scoping}
 
 A C Enum can be scoped, using @'!'@, so the enumerator constants are not projected into the enclosing scope.
@@ -64,5 +64,5 @@
 }
 \end{cfa}
-As in Section~\ref{s:EnumeratorVisibility}, opening multiple scoped enumerations in a @with@ can result in duplicate enumeration names, but \CFA implicit type resolution and explicit qualification/casting handle this localized scenario.
+As in Section~\ref{s:CVisibility}, opening multiple scoped enumerations in a @with@ can result in duplicate enumeration names, but \CFA implicit type resolution and explicit qualification/casting handle this localized scenario.
 
 A partially implemented extension to enumerator scoping is providing a combination of scoped and unscoped enumerators, using individual denotations, where @'^'@ means unscoped.
Index: doc/theses/jiada_liang_MMath/CFAenum.tex
===================================================================
--- doc/theses/jiada_liang_MMath/CFAenum.tex	(revision af5baae0adea725769db51743818a97dfe619952)
+++ doc/theses/jiada_liang_MMath/CFAenum.tex	(revision 0c51c8b42a007627bcf2537dfce73151c5a015ef)
@@ -6,7 +6,7 @@
 
 
-\section{Enumeration Syntax}
-
-\CFA extends the C enumeration declaration \see{\VRef{s:CEnumeration}} by parameterizing with a type (like a generic type), and adding Plan-9 inheritance \see{\VRef{s:EnumerationInheritance}} using an @inline@ to another enumeration type.
+\section{Syntax}
+
+\CFA extends the C enumeration declaration \see{\VRef{s:CEnumeration}} by parameterizing with a type (like a generic type), and adding Plan-9 inheritance \see{\VRef{s:CFAInheritance}} using an @inline@ to another enumeration type.
 \begin{cfa}[identifierstyle=\linespread{0.9}\it]
 $\it enum$-specifier:
@@ -24,5 +24,5 @@
 
 
-\section{Enumeration Operations}
+\section{Operations}
 
 \CFA enumerations have access to the three enumerations properties \see{\VRef{s:Terminology}}: label, order (position), and value via three overloaded functions @label@, @posn@, and @value@ \see{\VRef{c:trait} for details}.
@@ -43,10 +43,11 @@
 A A @0@ 3
 \end{cfa}
-Finally, there is an additional enumeration routine @countof@ (like @sizeof@, @typeof@) that returns the number of enumerators in an enumeration.
-\begin{cfa}
-enum(int) E { A, B, C, D };
-countof( E );  // 4
-\end{cfa}
-This auto-generated function replaces the C idiom for automatically computing the number of enumerators \see{\VRef{s:Usage}}.
+Finally, there is an additional enumeration pseudo-function @countof@ (like @sizeof@, @typeof@) that returns the number of enumerators in an enumeration.
+\begin{cfa}
+enum(int) E { A, B, C, D } e;
+countof( E );  // 4, type argument
+countof( e );  // 4, variable argument
+\end{cfa}
+This buildin function replaces the C idiom for automatically computing the number of enumerators \see{\VRef{s:Usage}}.
 \begin{cfa}
 enum E { A, B, C, D, @N@ };  // N == 4
@@ -197,11 +198,22 @@
 
 
-\section{Enumeration Inheritance}
-\label{s:EnumerationInheritance}
+\section{Subset}
+
+An enumeration's type can be another enumeration.
+\begin{cfa}
+enum( char ) Letter { A = 'A', ... };
+enum( @Letter@ ) Greek { Alph = A, Beta = B, ... }; // alphabet intersection
+\end{cfa}
+Enumeration @Greek@ may have more or less enums than @Letter@, but the enum values \emph{must} be from @Letter@.
+Therefore, @Greek@ enums are a subset of type @Letter@ and are type compatible with enumeration @Letter@, but @Letter@ enums are not type compatible with enumeration @Greek@.
+
+
+\section{Inheritance}
+\label{s:CFAInheritance}
 
 \CFA Plan-9 inheritance may be used with \CFA enumerations, where Plan-9 inheritance is containment inheritance with implicit unscoping (like a nested unnamed @struct@/@union@ in C).
 Containment is nominative: an enumeration inherits all enumerators from another enumeration by declaring an @inline statement@ in its enumerator lists.
 \begin{cfa}
-enum( char * ) Names { /* $\see{\VRef[Figure]{s:EnumerationInheritance}}$ */ };
+enum( char * ) Names { /* $\see{\VRef[Figure]{f:EumeratorTyping}}$ */ };
 enum( char * ) Names2 { @inline Names@, Jack = "JACK", Jill = "JILL" };
 enum( char * ) Names3 { @inline Names2@, Sue = "SUE", Tom = "TOM" };
@@ -302,5 +314,5 @@
 
 
-\section{Enumerator Control Structures}
+\section{Control Structures}
 
 Enumerators can be used in multiple contexts.
@@ -392,5 +404,5 @@
 
 
-\section{Enumeration Dimension}
+\section{Dimension}
 
 \VRef{s:EnumeratorTyping} introduces the harmonizing problem between an enumeration and secondary information.
@@ -420,5 +432,5 @@
 
 
-\section{Enumeration I/O}
+\section{I/O}
 
 As seen in multiple examples, enumerations can be printed and the default property printed is the enumerator's label, which is similar in other programming languages.
@@ -473,5 +485,4 @@
 \label{f:EnumerationI/O}
 \end{figure}
-
 
 
Index: doc/theses/jiada_liang_MMath/background.tex
===================================================================
--- doc/theses/jiada_liang_MMath/background.tex	(revision af5baae0adea725769db51743818a97dfe619952)
+++ doc/theses/jiada_liang_MMath/background.tex	(revision 0c51c8b42a007627bcf2537dfce73151c5a015ef)
@@ -232,9 +232,4 @@
 While C provides a true enumeration, it is restricted, has unsafe semantics, and does not provide useful/advanced enumeration features found in other programming languages.
 
-\section{\CFA Polymorphism}
-
-\subsection{Function Overloading}
-Function overloading is programming languages feature wherein functions may share the same name, but with different function signatures. In both C++ and \CFA, function names can be overloaded
-with different entities as long as they are different in terms of the number and type of parameters.
 
 \section{\CFA}
@@ -253,5 +248,5 @@
 Experience from \CC and \CFA developers is that the type system implicitly and correctly disambiguates the majority of overloaded names, \ie it is rare to get an incorrect selection or ambiguity, even among hundreds of overloaded (variables and) functions.
 In many cases, a programmer has no idea there are name clashes, as they are silently resolved, simplifying the development process.
-Depending on the language, ambiguous cases are resolved using some form of qualification or casting.
+Depending on the language, ambiguous cases are resolved using some form of qualification and/or casting.
 
 
@@ -269,5 +264,5 @@
 \end{cfa}
 The type system examines each call size and selects the best matching overloaded function based on the number and types of the arguments.
-If there are intermixed operands, @2 + 3.5@, the type system attempts (safe) conversions changing the arguments to one or more of the parameter type(s).
+If there are mixed-mode operands, @2 + 3.5@, the type system, like in C/\CC, attempts (safe) conversions, converting the argument type(s) to the parameter type(s).
 
 
@@ -282,5 +277,5 @@
 \end{cfa}
 In this case, the name @f@ is overloaded depending on the number and parameter types.
-The type system examines each call size and selects the best matching based on the number and types of the arguments.
+The type system examines each call size and selects the best match based on the number and types of the arguments.
 Here, there is a perfect match for the call, @f( 'A' )@ with the number and parameter type of function (2).
 
@@ -321,5 +316,5 @@
 
 The prototype for the constructor/destructor are @void ?{}( T &, ... )@ and @void ^?{}( T &, ... )@, respectively.
-The first parameter is logically, the \lstinline[language=C++]{this} or \lstinline[language=Python]{self} in other object-oriented languages, and implicitly passed.
+The first parameter is logically the \lstinline[language=C++]{this} or \lstinline[language=Python]{self} in other object-oriented languages, and implicitly passed.
 \VRef[Figure]{f:CFAConstructorDestructor} shows an example of creating and using a constructor and destructor.
 Both constructor and destructor can be explicitly called to reuse a variable.
@@ -391,13 +386,11 @@
 \end{cfa}
 The assertion on @T@ restricts the range of types that can be manipulated by @bar@ to only those that have an implementation of @foo@ with the matching signature, allowing @bar@'s call to @foo@ in its body.
+Unlike templates in \CC, which are macro expansions at the call site, \CFA polymorphic functions are compiled, passing the call-site assertion functions as hidden parameters.
+
 
 \subsection{Trait}
-A @forall@ clause can asserts on multiple types and with multiple asserting functions. A common practice in \CFA is to group
-the asserting functions in to a named \newterm{trait}.
-
-\subsection{Trait}
 
 A @forall@ clause can assert many restrictions on multiple types.
-A common practice is to refactor the assertions into a named \newterm{trait}.
+A common practice is to refactor the assertions into a named \newterm{trait}, similar to other lnaguages, like Go and Rust.
 \begin{cfa}
 forall(T) trait @Bird@ {
@@ -432,5 +425,5 @@
 
 Most programming languages perform some implicit conversions among basic types to facilitate mixed-mode arithmetic;
-otherwise, the program becomes littered with many explicit casts, which is not match programmer expectation.
+otherwise, the program becomes littered with many explicit casts, which does not match with programmer expectation.
 C is an aggressive language as it provides conversions among almost all of the basic types, even when the conversion is potentially unsafe or not meaningful, \ie @float@ to @bool@.
 C defines the resolution pattern as ``usual arithmetic conversion''~\cite[\S~6.3.1.8]{C11}, in which C looks for a \newterm{common type} between operands, and converts one or both operands to the common type.
Index: doc/theses/jiada_liang_MMath/intro.tex
===================================================================
--- doc/theses/jiada_liang_MMath/intro.tex	(revision af5baae0adea725769db51743818a97dfe619952)
+++ doc/theses/jiada_liang_MMath/intro.tex	(revision 0c51c8b42a007627bcf2537dfce73151c5a015ef)
@@ -299,13 +299,17 @@
 \begin{enumerate}
 \item
-overloading: provides a pattern to overload functions, literal, and variable for polymorphic enumerations.
-\item
-scoping: adds name space for enumerations.
-\item
-safety: defines a safe enumeration conversion scheme.
-\item
-harmonization: allows enumeration to be mapped with data.
-\item
-inheritance: implements containment inheritance for enumerations.
+safety: Define a safe enumeration conversion scheme, both for C and \CFA, and replace ad-hoc C idioms with safer software-engineering approaches.
+\item
+overloading: Provide a pattern to overload functions, literals, and variables for polymorphic enumerations using the \CFA type system.
+\item
+scoping: Add a name space for enumerations and qualified access into the namespace to deal with the naming problem.
+\item
+generalization: Support all language types for enumerators with associated values providing enumeration constants for any type.
+\item
+inheritance: Implement subtyping and containment inheritance for enumerations.
+\item
+control flow: Extend control-flow structures making it safer and easier to enumerate over an enumeration.
+\item
+I/O: Provide input and output of enumerations based on enumerator names.
 \end{enumerate}