Index: doc/theses/jiada_liang_MMath/background.tex
===================================================================
--- doc/theses/jiada_liang_MMath/background.tex	(revision 2514d3d7ef96e399511360e31eade8b765af57fa)
+++ doc/theses/jiada_liang_MMath/background.tex	(revision 5fdaeab1e503d76454d1dc8edc3fd1025c76013d)
@@ -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.
