Index: doc/papers/general/Paper.tex
===================================================================
--- doc/papers/general/Paper.tex	(revision 28bc8c8060f9366d54baea1d0ac5681a7a636197)
+++ doc/papers/general/Paper.tex	(revision 9d6f01107c8342a25c608f400abd14da5ecabede)
@@ -267,4 +267,5 @@
 int m = max( max, -max );					$\C{// uses (3) and (1) twice, by matching return type}$
 \end{cfa}
+
 \CFA maximizes the ability to reuse names to aggressively address the naming problem.
 In some cases, hundreds of names can be reduced to tens, resulting in a significant cognitive reduction.
@@ -285,5 +286,5 @@
 
 
-\subsection{\texorpdfstring{\LstKeywordStyle{forall} Functions}{forall Functions}}
+\subsection{\texorpdfstring{\protect\lstinline{forall} Functions}{forall Functions}}
 \label{sec:poly-fns}
 
@@ -435,5 +436,5 @@
 One approach is to write bespoke data-structures for each context in which they are needed.
 While this approach is flexible and supports integration with the C type-checker and tooling, it is also tedious and error-prone, especially for more complex data structures.
-A second approach is to use @void *@--based polymorphism, \eg the C standard-library functions @bsearch@ and @qsort@, which allow reuse of code with common functionality.
+A second approach is to use @void *@ based polymorphism, \eg the C standard-library functions @bsearch@ and @qsort@, which allow reuse of code with common functionality.
 However, basing all polymorphism on @void *@ eliminates the type-checker's ability to ensure that argument types are properly matched, often requiring a number of extra function parameters, pointer indirection, and dynamic allocation that is not otherwise needed.
 A third approach to generic code is to use preprocessor macros, which does allow the generated code to be both generic and type-checked, but errors may be difficult to interpret.
@@ -507,13 +508,13 @@
 The offset arrays are statically generated where possible.
 If a dynamic generic-type is declared to be passed or returned by value from a polymorphic function, the translator can safely assume the generic type is complete (\ie has a known layout) at any call-site, and the offset array is passed from the caller;
-if the generic type is concrete at the call site, the elements of this offset array can even be statically generated using the C @offsetof@ macro. 
-As an example, the body of the second @value@ function is implemented like this:
-\begin{cfa}
-_assign_T(_retval, p + _offsetof_pair[1]); $\C{// return *p.second}$
-\end{cfa}
-@_assign_T@ is passed in as an implicit parameter from @otype T@, and takes two @T*@ (@void*@ in the generated code), a destination and a source; @_retval@ is the pointer to a caller-allocated buffer for the return value, the usual \CFA method to handle dynamically-sized return types.
+if the generic type is concrete at the call site, the elements of this offset array can even be statically generated using the C @offsetof@ macro.
+As an example, the body of the second @value@ function is implemented as:
+\begin{cfa}
+_assign_T( _retval, p + _offsetof_pair[1] ); $\C{// return *p.second}$
+\end{cfa}
+@_assign_T@ is passed in as an implicit parameter from @otype T@, and takes two @T *@ (@void *@ in the generated code), a destination and a source; @_retval@ is the pointer to a caller-allocated buffer for the return value, the usual \CFA method to handle dynamically-sized return types.
 @_offsetof_pair@ is the offset array passed into @value@; this array is generated at the call site as:
 \begin{cfa}
-size_t _offsetof_pair[] = { offsetof(_pair_conc0, first), offsetof(_pair_conc0, second) }
+size_t _offsetof_pair[] = { offsetof( _pair_conc0, first ), offsetof( _pair_conc0, second ) }
 \end{cfa}
 
@@ -539,18 +540,18 @@
 The most important such pattern is using @forall(dtype T) T *@ as a type-checked replacement for @void *@, \eg creating a lexicographic comparison for pairs of pointers used by @bsearch@ or @qsort@:
 \begin{cfa}
-forall(dtype T) int lexcmp( pair( T *, T * ) * a, pair( T *, T * ) * b, int (* cmp)( T *, T * ) ) {
+forall( dtype T ) int lexcmp( pair( T *, T * ) * a, pair( T *, T * ) * b, int (* cmp)( T *, T * ) ) {
 	return cmp( a->first, b->first ) ? : cmp( a->second, b->second );
 }
 \end{cfa}
-Since @pair(T *, T * )@ is a concrete type, there are no implicit parameters passed to @lexcmp@, so the generated code is identical to a function written in standard C using @void *@, yet the \CFA version is type-checked to ensure the fields of both pairs and the arguments to the comparison function match in type.
+Since @pair( T *, T * )@ is a concrete type, there are no implicit parameters passed to @lexcmp@, so the generated code is identical to a function written in standard C using @void *@, yet the \CFA version is type-checked to ensure the fields of both pairs and the arguments to the comparison function match in type.
 
 Another useful pattern enabled by reused dtype-static type instantiations is zero-cost \newterm{tag-structures}.
 Sometimes information is only used for type-checking and can be omitted at runtime, \eg:
 \begin{cfa}
-forall(dtype Unit) struct scalar { unsigned long value; };
+forall( dtype Unit ) struct scalar { unsigned long value; };
 struct metres {};
 struct litres {};
 
-forall(dtype U) scalar(U) ?+?( scalar(U) a, scalar(U) b ) {
+forall( dtype U ) scalar(U) ?+?( scalar(U) a, scalar(U) b ) {
 	return (scalar(U)){ a.value + b.value };
 }
@@ -807,5 +808,5 @@
 Due to the implicit flattening and structuring conversions involved in argument passing, @otype@ and @dtype@ parameters are restricted to matching only with non-tuple types, \eg:
 \begin{cfa}
-forall(otype T, dtype U) void f( T x, U * y );
+forall( otype T, dtype U ) void f( T x, U * y );
 f( [5, "hello"] );
 \end{cfa}
@@ -814,5 +815,5 @@
 For example, a plus operator can be written to add two triples together.
 \begin{cfa}
-forall(otype T | { T ?+?( T, T ); }) [T, T, T] ?+?( [T, T, T] x, [T, T, T] y ) {
+forall( otype T | { T ?+?( T, T ); } ) [T, T, T] ?+?( [T, T, T] x, [T, T, T] y ) {
 	return [x.0 + y.0, x.1 + y.1, x.2 + y.2];
 }
@@ -825,15 +826,15 @@
 \begin{cfa}
 int f( [int, double], double );
-forall(otype T, otype U | { T f( T, U, U ); }) void g( T, U );
+forall( otype T, otype U | { T f( T, U, U ); } ) void g( T, U );
 g( 5, 10.21 );
 \end{cfa}
 Hence, function parameter and return lists are flattened for the purposes of type unification allowing the example to pass expression resolution.
 This relaxation is possible by extending the thunk scheme described by Bilson~\cite{Bilson03}.
-Whenever a candidate's parameter structure does not exactly match the formal parameter's structure, a thunk is generated to specialize calls to the actual function:
-\begin{cfa}
-int _thunk( int _p0, double _p1, double _p2 ) { return f( [_p0, _p1], _p2 ); }
-\end{cfa}
-so the thunk provides flattening and structuring conversions to inferred functions, improving the compatibility of tuples and polymorphism.
-These thunks take advantage of gcc C nested-functions to produce closures that have the usual function-pointer signature WHAT DOES THIS MEAN???.
+% Whenever a candidate's parameter structure does not exactly match the formal parameter's structure, a thunk is generated to specialize calls to the actual function:
+% \begin{cfa}
+% int _thunk( int _p0, double _p1, double _p2 ) { return f( [_p0, _p1], _p2 ); }
+% \end{cfa}
+% so the thunk provides flattening and structuring conversions to inferred functions, improving the compatibility of tuples and polymorphism.
+% These thunks are generated locally using gcc nested-functions, rather hositing them to the external scope, so they can easily access local state.
 
 
@@ -852,5 +853,5 @@
 \begin{cfa}
 int sum$\(_0\)$() { return 0; }
-forall(ttype Params | { int sum( Params ); } ) int sum$\(_1\)$( int x, Params rest ) {
+forall( ttype Params | { int sum( Params ); } ) int sum$\(_1\)$( int x, Params rest ) {
 	return x + sum( rest );
 }
@@ -865,5 +866,5 @@
 \begin{cfa}
 int sum( int x, int y ) { return x + y; }
-forall(ttype Params | { int sum( int, Params ); } ) int sum( int x, int y, Params rest ) {
+forall( ttype Params | { int sum( int, Params ); } ) int sum( int x, int y, Params rest ) {
 	return sum( x + y, rest );
 }
@@ -871,11 +872,11 @@
 One more step permits the summation of any summable type with all arguments of the same type:
 \begin{cfa}
-trait summable(otype T) {
+trait summable( otype T ) {
 	T ?+?( T, T );
 };
-forall(otype R | summable( R ) ) R sum( R x, R y ) {
+forall( otype R | summable( R ) ) R sum( R x, R y ) {
 	return x + y;
 }
-forall(otype R, ttype Params | summable(R) | { R sum(R, Params); } ) R sum(R x, R y, Params rest) {
+forall( otype R, ttype Params | summable(R) | { R sum(R, Params); } ) R sum(R x, R y, Params rest) {
 	return sum( x + y, rest );
 }
@@ -888,5 +889,5 @@
 \begin{cfa}
 struct S { int x, y; };
-forall(otype T, ttype Params | { void print(T); void print(Params); }) void print(T arg, Params rest) {
+forall( otype T, ttype Params | { void print(T); void print(Params); } ) void print(T arg, Params rest) {
 	print(arg);  print(rest);
 }
@@ -927,5 +928,5 @@
 is transformed into:
 \begin{cfa}
-forall(dtype T0, dtype T1 | sized(T0) | sized(T1)) struct _tuple2 {
+forall( dtype T0, dtype T1 | sized(T0) | sized(T1) ) struct _tuple2 {
 	T0 field_0;								$\C{// generated before the first 2-tuple}$
 	T1 field_1;
@@ -933,5 +934,5 @@
 _tuple2(int, int) f() {
 	_tuple2(double, double) x;
-	forall(dtype T0, dtype T1, dtype T2 | sized(T0) | sized(T1) | sized(T2)) struct _tuple3 {
+	forall( dtype T0, dtype T1, dtype T2 | sized(T0) | sized(T1) | sized(T2) ) struct _tuple3 {
 		T0 field_0;							$\C{// generated before the first 3-tuple}$
 		T1 field_1;
@@ -941,7 +942,7 @@
 }
 \end{cfa}
-\begin{sloppypar}
+{\sloppy
 Tuple expressions are then simply converted directly into compound literals, \eg @[5, 'x', 1.24]@ becomes @(_tuple3(int, char, double)){ 5, 'x', 1.24 }@.
-\end{sloppypar}
+\par}%
 
 \begin{comment}
@@ -1004,8 +1005,8 @@
 \section{Control Structures}
 
-\CFA identifies inconsistent, problematic, and missing control structures in C, and extends, modifies, and adds to control structures to increase functionality and safety.
-
-
-\subsection{\texorpdfstring{\LstKeywordStyle{if} Statement}{if Statement}}
+\CFA identifies inconsistent, problematic, and missing control structures in C, and extends, modifies, and adds control structures to increase functionality and safety.
+
+
+\subsection{\texorpdfstring{\protect\lstinline{if} Statement}{if Statement}}
 
 The @if@ expression allows declarations, similar to @for@ declaration expression:
@@ -1019,5 +1020,5 @@
 
 
-\subsection{\texorpdfstring{\LstKeywordStyle{switch} Statement}{switch Statement}}
+\subsection{\texorpdfstring{\protect\lstinline{switch} Statement}{switch Statement}}
 
 There are a number of deficiencies with the C @switch@ statements: enumerating @case@ lists, placement of @case@ clauses, scope of the switch body, and fall through between case clauses.
@@ -1039,5 +1040,5 @@
 \lstMakeShortInline@%
 \end{cquote}
-for a contiguous list:\footnote{gcc provides the same mechanism with awkward syntax, \lstinline@2 ... 42@, where spaces are required around the ellipse.}
+for a contiguous list:\footnote{gcc has the same mechanism but awkward syntax, \lstinline@2 ...42@, because a space is required after a number, otherwise the period is a decimal point.}
 \begin{cquote}
 \lstDeleteShortInline@%
@@ -1090,8 +1091,6 @@
 C @switch@ provides multiple entry points into the statement body, but once an entry point is selected, control continues across \emph{all} @case@ clauses until the end of the @switch@ body, called \newterm{fall through};
 @case@ clauses are made disjoint by the @break@ statement.
-While the ability to fall through \emph{is} a useful form of control flow, it does not match well with programmer intuition, resulting in many errors from missing @break@ statements.
-For backwards compatibility, \CFA provides a \emph{new} control structure, @choose@, which mimics @switch@, but reverses the meaning of fall through (see Figure~\ref{f:ChooseSwitchStatements}).
-
-Collectively, these enhancements reduce programmer burden and increase readability and safety.
+While fall through \emph{is} a useful form of control flow, it does not match well with programmer intuition, resulting in errors from missing @break@ statements.
+For backwards compatibility, \CFA provides a \emph{new} control structure, @choose@, which mimics @switch@, but reverses the meaning of fall through (see Figure~\ref{f:ChooseSwitchStatements}), similar to Go.
 
 \begin{figure}
@@ -1137,29 +1136,41 @@
 \end{figure}
 
-\begin{comment}
-Forgotten @break@ statements at the end of @switch@ cases are a persistent sort of programmer error in C, and the @break@ statements themselves introduce visual clutter and an un-C-like keyword-based block delimiter. 
-\CFA addresses this error by introducing a @choose@ statement, which works identically to a @switch@ except that its default end-of-case behaviour is to break rather than to fall through for all non-empty cases. 
-Since empty cases like @case 7:@ in @case 7: case 11:@ still have fall-through semantics and explicit @break@ is still allowed at the end of a @choose@ case, many idiomatic uses of @switch@ in standard C can be converted to @choose@ statements by simply changing the keyword. 
-Where fall-through is desired for a non-empty case, it can be specified with the new @fallthrough@ statement, making @choose@ equivalently powerful to @switch@, but more concise in the common case where most non-empty cases end with a @break@ statement, as in the example below:
-
-\begin{cfa}
-choose( i ) {
-	case 2:
-		printf("even ");
-		fallthrough;
-	case 3: case 5: case 7:
-		printf("small prime\n");
-	case 4,6,8,9:
-		printf("small composite\n");
-	case 13~19:
-		printf("teen\n");
-	default:
-		printf("something else\n");
-}
-\end{cfa}
-\end{comment}
-
-
-\subsection{\texorpdfstring{Labelled \LstKeywordStyle{continue} / \LstKeywordStyle{break}}{Labelled continue / break}}
+Finally, @fallthrough@ may appear in contexts other than terminating a @case@ clause, and have an explicit transfer label allowing separate cases but common final-code for a set of cases:
+\begin{cquote}
+\lstDeleteShortInline@%
+\begin{tabular}{@{}l@{\hspace{2\parindentlnth}}l@{}}
+\multicolumn{1}{c@{\hspace{2\parindentlnth}}}{\textbf{non-terminator}}	& \multicolumn{1}{c}{\textbf{target label}}	\\
+\begin{cfa}
+choose ( ... ) {
+  case 3:
+	if ( ... ) {
+		... `fallthrough;`  // goto case 4
+	} else {
+		...
+	}
+	// implicit break
+  case 4:
+\end{cfa}
+&
+\begin{cfa}
+choose ( ... ) {
+  case 3:
+	... `fallthrough common;`
+  case 4:
+	... `fallthrough common;`
+  common:
+	...	 // common code for cases 3 and 4
+	// implicit break
+  case 4:
+\end{cfa}
+\end{tabular}
+\lstMakeShortInline@%
+\end{cquote}
+The target label may be case @default@.
+
+Collectively, these control-structure enhancements reduce programmer burden and increase readability and safety.
+
+
+\subsection{\texorpdfstring{Labelled \protect\lstinline{continue} / \protect\lstinline{break}}{Labelled continue / break}}
 
 While C provides @continue@ and @break@ statements for altering control flow, both are restricted to one level of nesting for a particular control structure.
@@ -1270,5 +1281,5 @@
 \subsection{Exception Handling}
 
-The following framework for \CFA exception handling is in place, excluding some run-time type-information and dynamic casts.
+The following framework for \CFA exception handling is in place, excluding some runtime type-information and virtual functions.
 \CFA provides two forms of exception handling: \newterm{fix-up} and \newterm{recovery} (see Figure~\ref{f:CFAExceptionHandling})~\cite{Buhr92b,Buhr00a}.
 Both mechanisms provide dynamic call to a handler using dynamic name-lookup, where fix-up has dynamic return and recovery has static return from the handler.
@@ -1340,5 +1351,5 @@
    catch ( IOError err ) { ... }			$\C{// handler error from other files}$
 \end{cfa}
-where the throw inserts the failing file-handle in the I/O exception.
+where the throw inserts the failing file-handle into the I/O exception.
 Conditional catch cannot be trivially mimicked by other mechanisms because once an exception is caught, handler clauses in that @try@ statement are no longer eligible..
 
@@ -1348,8 +1359,8 @@
 resume( $\emph{alternate-stack}$ )
 \end{cfa}
-These overloads of @resume@ raise the specified exception or the currently propagating exception (reresume) at another \CFA coroutine or task~\cite{Delisle18}.\footnote{\CFA coroutine and concurrency features are discussed in a separately submitted paper.}
-Nonlocal raise is restricted to resumption to provide the exception handler the greatest flexibility because processing the exception does not unwind its stack, allowing it to continue after the handle returns.
-
-To facilitate nonlocal exception, \CFA provides dynamic enabling and disabling of nonlocal exception-propagation.
+These overloads of @resume@ raise the specified exception or the currently propagating exception (reresume) at another \CFA coroutine or task\footnote{\CFA coroutine and concurrency features are discussed in a separately submitted paper.}~\cite{Delisle18}.
+Nonlocal raise is restricted to resumption to provide the exception handler the greatest flexibility because processing the exception does not unwind its stack, allowing it to continue after the handler returns.
+
+To facilitate nonlocal raise, \CFA provides dynamic enabling and disabling of nonlocal exception-propagation.
 The constructs for controlling propagation of nonlocal exceptions are the @enable@ and the @disable@ blocks:
 \begin{cquote}
@@ -1358,5 +1369,5 @@
 \begin{cfa}
 enable $\emph{exception-type-list}$ {
-	// allow non-local resumption
+	// allow non-local raise
 }
 \end{cfa}
@@ -1364,5 +1375,5 @@
 \begin{cfa}
 disable $\emph{exception-type-list}$ {
-	// disallow non-local resumption
+	// disallow non-local raise
 }
 \end{cfa}
@@ -1375,10 +1386,11 @@
 Coroutines and tasks start with non-local exceptions disabled, allowing handlers to be put in place, before non-local exceptions are explicitly enabled.
 \begin{cfa}
-void main( mytask & c ) {
-	try {
-		enable {			$\C{// now allow non-local exception delivery}$
+void main( mytask & t ) {					$\C{// thread starts here}$
+	// non-local exceptions disabled
+	try {									$\C{// establish handles for non-local exceptions}$
+		enable {							$\C{// allow non-local exception delivery}$
 			// task body
 		}
-	// appropriate catchResume/catch
+	// appropriate catchResume/catch handlers
 	}
 }
@@ -1400,5 +1412,5 @@
 
 
-\subsection{\texorpdfstring{\LstKeywordStyle{with} Clause / Statement}{with Clause / Statement}}
+\subsection{\texorpdfstring{\protect\lstinline{with} Clause / Statement}{with Clause / Statement}}
 \label{s:WithClauseStatement}
 
@@ -1800,5 +1812,5 @@
 int & r = *new( int );
 ...											$\C{// non-null reference}$
-delete &r;
+delete &r;									$\C{// unmanaged (programmer) memory-management}$
 r += 1;										$\C{// undefined reference}$
 \end{cfa}
@@ -1947,7 +1959,7 @@
 Constructor calls seamlessly integrate with existing C initialization syntax, providing a simple and familiar syntax to C programmers and allowing constructor calls to be inserted into legacy C code with minimal code changes.
 
-In \CFA, a constructor is named @?{}@ and a destructor is named @^?{}@.
-The name @{}@ comes from the syntax for the initializer: @struct S { int i, j; } s = `{` 2, 3 `}`@\footnote{%
+In \CFA, a constructor is named @?{}@ and a destructor is named @^?{}@\footnote{%
 The symbol \lstinline+^+ is used for the destructor name because it was the last binary operator that could be used in a unary context.}.
+The name @{}@ comes from the syntax for the initializer: @struct S { int i, j; } s = `{` 2, 3 `}`@.
 Like other \CFA operators, these names represent the syntax used to call the constructor or destructor, \eg @?{}(x, ...)@ or @^{}(x, ...)@.
 The constructor and destructor have return type @void@, and the first parameter is a reference to the object type to be constructed or destructed.
@@ -2071,14 +2083,21 @@
 \subsection{0/1}
 
-In C, @0@ has the special property that it is the only ``false'' value; by the standard, any value which compares equal to @0@ is false, while any value that compares unequal to @0@ is true. 
-As such, an expression @x@ in any boolean context (such as the condition of an @if@ or @while@ statement, or the arguments to @&&@, @||@, or @?:@) can be rewritten as @x != 0@ without changing its semantics.
-The operator overloading feature of \CFA provides a natural means to implement this truth value comparison for arbitrary types, but the C type system is not precise enough to distinguish an equality comparison with @0@ from an equality comparison with an arbitrary integer or pointer. 
-To provide this precision, \CFA introduces a new type @zero_t@ as type type of literal @0@ (somewhat analagous to @nullptr_t@ and @nullptr@ in \CCeleven); @zero_t@ can only take the value @0@, but has implicit conversions to the integer and pointer types so that C code involving @0@ continues to work properly. 
-With this addition, the \CFA compiler rewrites @if (x)@ and similar expressions to @if ((x) != 0)@ or the appropriate analogue, and any type @T@ can be made ``truthy'' by defining an operator overload @int ?!=?(T, zero_t)@.
-\CC makes types truthy by adding a conversion to @bool@; prior to the addition of explicit cast operators in \CCeleven this approach had the pitfall of making truthy types transitively convertable to any numeric type; our design for \CFA avoids this issue.
-
-\CFA also includes a special type for @1@, @one_t@; like @zero_t@, @one_t@ has built-in implicit conversions to the various integral types so that @1@ maintains its expected semantics in legacy code. 
-The addition of @one_t@ allows generic algorithms to handle the unit value uniformly for types where that is meaningful. 
-\TODO{Make this sentence true} In particular, polymorphic functions in the \CFA prelude define @++x@ and @x++@ in terms of @x += 1@, allowing users to idiomatically define all forms of increment for a type @T@ by defining the single function @T & ?+=(T &, one_t)@; analogous overloads for the decrement operators are present as well.
+In C, @0@ has the special property that it is the only ``false'' value;
+from the standard, any value that compares equal to @0@ is false, while any value that compares unequal to @0@ is true. 
+As such, an expression @x@ in any boolean context (such as the condition of an @if@ or @while@ statement, or the arguments to @&&@, @||@, or @?:@\,) can be rewritten as @x != 0@ without changing its semantics.
+Operator overloading in \CFA provides a natural means to implement this truth-value comparison for arbitrary types, but the C type system is not precise enough to distinguish an equality comparison with @0@ from an equality comparison with an arbitrary integer or pointer. 
+To provide this precision, \CFA introduces a new type @zero_t@ as the type of literal @0@ (somewhat analagous to @nullptr_t@ and @nullptr@ in \CCeleven);
+@zero_t@ can only take the value @0@, but has implicit conversions to the integer and pointer types so that C code involving @0@ continues to work. 
+With this addition, \CFA rewrites @if (x)@ and similar expressions to @if ((x) != 0)@ or the appropriate analogue, and any type @T@ is ``truthy'' by defining an operator overload @int ?!=?(T, zero_t)@.
+\CC makes types truthy by adding a conversion to @bool@;
+prior to the addition of explicit cast operators in \CCeleven, this approach had the pitfall of making truthy types transitively convertable to any numeric type;
+\CFA avoids this issue.
+
+Similarly, \CFA also has a special type for @1@, @one_t@;
+like @zero_t@, @one_t@ has built-in implicit conversions to the various integral types so that @1@ maintains its expected semantics in legacy code for operations @++@ and @--@.
+The addition of @one_t@ allows generic algorithms to handle the unit value uniformly for types where it is meaningful.
+\TODO{Make this sentence true}
+In particular, polymorphic functions in the \CFA prelude define @++x@ and @x++@ in terms of @x += 1@, allowing users to idiomatically define all forms of increment for a type @T@ by defining the single function @T & ?+=(T &, one_t)@;
+analogous overloads for the decrement operators are present as well.
 
 
@@ -2088,5 +2107,5 @@
 The left of Figure~\ref{f:UserLiteral} shows the \CFA alternative call-syntax (literal argument before function name), using the backquote, to convert basic literals into user literals.
 The backquote is a small character, making the unit (function name) predominate.
-For examples, the multi-precision integers in Section~\ref{s:MultiPrecisionIntegers} make use of user literals:
+For examples, the multi-precision integer-type in Section~\ref{s:MultiPrecisionIntegers} has user literals:
 {\lstset{language=CFA,moredelim=**[is][\color{red}]{|}{|},deletedelim=**[is][]{`}{`}}
 \begin{cfa}
@@ -2308,5 +2327,5 @@
 \lstMakeShortInline@%
 \end{cquote}
-In additon, there are polymorphic functions, like @min@ and @max@, which work on any type with operators @?<?@ or @?>?@.
+In additon, there are polymorphic functions, like @min@ and @max@, that work on any type with operators @?<?@ or @?>?@.
 
 The following shows one example where \CFA \emph{extends} an existing standard C interface to reduce complexity and provide safety.
@@ -2319,8 +2338,8 @@
 In either case, new storage may or may not be allocated and, if there is a new allocation, as much data from the existing allocation is copied.
 For an increase in storage size, new storage after the copied data may be filled.
-\item[alignment]
+\item[align]
 an allocation on a specified memory boundary, \eg, an address multiple of 64 or 128 for cache-line purposes.
 \item[array]
-allocation of the specified number of elements.
+allocation with a specified number of elements.
 An array may be filled, resized, or aligned.
 \end{description}
@@ -2334,5 +2353,5 @@
 \lstMakeShortInline~%
 \begin{tabular}{@{}r|r|l|l|l|l@{}}
-\multicolumn{1}{c}{}&		& \multicolumn{1}{c|}{fill}	& resize	& alignment	& array	\\
+\multicolumn{1}{c}{}&		& \multicolumn{1}{c|}{fill}	& resize	& align	& array	\\
 \hline
 C		& ~malloc~			& no			& no		& no		& no	\\
@@ -2562,6 +2581,5 @@
 	TIMED( "copy_int", ti{ si }; )
 	TIMED( "clear_int", clear( si ); )
-	REPEAT_TIMED( "pop_int", N, 
-		int x = pop( ti ); if ( x > max ) max = x; )
+	REPEAT_TIMED( "pop_int", N, int x = pop( ti ); if ( x > max ) max = x; )
 
 	pair( short, char ) max = { 0h, '\0' }, val = { 42h, 'a' };
@@ -2571,6 +2589,5 @@
 	TIMED( "copy_pair", tp{ sp }; )
 	TIMED( "clear_pair", clear( sp ); )
-	REPEAT_TIMED( "pop_pair", N,
-		pair(short, char) x = pop( tp ); if ( x > max ) max = x; )
+	REPEAT_TIMED( "pop_pair", N, pair(short, char) x = pop( tp ); if ( x > max ) max = x; )
 }
 \end{cfa}
@@ -2605,5 +2622,5 @@
 									& \CT{C}	& \CT{\CFA}	& \CT{\CC}	& \CT{\CCV}		\\ \hline
 maximum memory usage (MB)			& 10001		& 2502		& 2503		& 11253			\\
-source code size (lines)			& 187		& 188		& 133		& 303			\\
+source code size (lines)			& 187		& 186		& 133		& 303			\\
 redundant type annotations (lines)	& 25		& 0			& 2			& 16			\\
 binary size (KB)					& 14		& 257		& 14		& 37			\\
@@ -2619,5 +2636,5 @@
 Finally, the binary size for \CFA is larger because of static linking with the \CFA libraries.
 
-\CFA is also competitive in terms of source code size, measured as a proxy for programmer effort. The line counts in Table~\ref{tab:eval} include implementations of @pair@ and @stack@ types for all four languages for purposes of direct comparison, though it should be noted that \CFA and \CC have pre-written data structures in their standard libraries that programmers would generally use instead. Use of these standard library types has minimal impact on the performance benchmarks, but shrinks the \CFA and \CC benchmarks to 41 and 42 lines, respectively.
+\CFA is also competitive in terms of source code size, measured as a proxy for programmer effort. The line counts in Table~\ref{tab:eval} include implementations of @pair@ and @stack@ types for all four languages for purposes of direct comparison, though it should be noted that \CFA and \CC have pre-written data structures in their standard libraries that programmers would generally use instead. Use of these standard library types has minimal impact on the performance benchmarks, but shrinks the \CFA and \CC benchmarks to 39 and 42 lines, respectively.
 On the other hand, C does not have a generic collections-library in its standard distribution, resulting in frequent reimplementation of such collection types by C programmers.
 \CCV does not use the \CC standard template library by construction, and in fact includes the definition of @object@ and wrapper classes for @char@, @short@, and @int@ in its line count, which inflates this count somewhat, as an actual object-oriented language would include these in the standard library;
@@ -2725,5 +2742,5 @@
 Finally, we demonstrate that \CFA performance for some idiomatic cases is better than C and close to \CC, showing the design is practically applicable.
 
-There is ongoing work on a wide range of \CFA feature extensions, including arrays with size, user-defined conversions, concurrent primitives, and modules.
+There is ongoing work on a wide range of \CFA feature extensions, including arrays with size, runtime type-information, virtual functions, user-defined conversions, 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 additional extensions.)
 In addition, there are interesting future directions for the polymorphism design.
@@ -2760,11 +2777,11 @@
 \CFA
 \begin{cfa}[xleftmargin=2\parindentlnth,aboveskip=0pt,belowskip=0pt]
-forall(otype T) struct stack_node {
+forall( otype T ) struct stack_node {
 	T value;
 	stack_node(T) * next;
 };
-forall(otype T) struct stack { stack_node(T) * head; };
-forall(otype T) void ?{}( stack(T) & s ) { (s.head){ 0 }; }
-forall(otype T) void ?{}( stack(T) & s, stack(T) t ) {
+forall( otype T ) struct stack { stack_node(T) * head; };
+forall( otype T ) void ?{}( stack(T) & s ) { (s.head){ 0 }; }
+forall( otype T ) void ?{}( stack(T) & s, stack(T) t ) {
 	stack_node(T) ** crnt = &s.head;
 	for ( stack_node(T) * next = t.head; next; next = next->next ) {
@@ -2775,5 +2792,5 @@
 	*crnt = 0;
 }
-forall(otype T) stack(T) ?=?( stack(T) & s, stack(T) t ) {
+forall( otype T ) stack(T) ?=?( stack(T) & s, stack(T) t ) {
 	if ( s.head == t.head ) return s;
 	clear( s );
@@ -2781,12 +2798,12 @@
 	return s;
 }
-forall(otype T) void ^?{}( stack(T) & s) { clear( s ); }
-forall(otype T) _Bool empty( const stack(T) & s ) { return s.head == 0; }
-forall(otype T) void push( stack(T) & s, T value ) {
+forall( otype T ) void ^?{}( stack(T) & s) { clear( s ); }
+forall( otype T ) _Bool empty( const stack(T) & s ) { return s.head == 0; }
+forall( otype T ) void push( stack(T) & s, T value ) with( s ) {
 	stack_node(T) * n = alloc();
 	(*n){ value, head };
 	head = n;
 }
-forall(otype T) T pop( stack(T) & s ) {
+forall( otype T ) T pop( stack(T) & s ) with( s ) {
 	stack_node(T) * n = head;
 	head = n->next;
@@ -2796,5 +2813,5 @@
 	return x;
 }
-forall(otype T) void clear( stack(T) & s ) {
+forall( otype T ) void clear( stack(T) & s ) with( s ) {
 	for ( stack_node(T) * next = head; next; ) {
 		stack_node(T) * crnt = next;
Index: doc/papers/general/evaluation/cfa-bench.c
===================================================================
--- doc/papers/general/evaluation/cfa-bench.c	(revision 28bc8c8060f9366d54baea1d0ac5681a7a636197)
+++ doc/papers/general/evaluation/cfa-bench.c	(revision 9d6f01107c8342a25c608f400abd14da5ecabede)
@@ -10,6 +10,5 @@
 	TIMED( "copy_int", ti{ si }; )
 	TIMED( "clear_int", clear( si ); )
-	REPEAT_TIMED( "pop_int", N, 
-		int x = pop( ti ); if ( x > max ) max = x; )
+	REPEAT_TIMED( "pop_int", N, int x = pop( ti ); if ( x > max ) max = x; )
 
 	pair( short, char ) max = { 0h, '\0' }, val = { 42h, 'a' };
@@ -19,5 +18,4 @@
 	TIMED( "copy_pair", tp{ sp }; )
 	TIMED( "clear_pair", clear( sp ); )
-	REPEAT_TIMED( "pop_pair", N,
-		pair(short, char) x = pop( tp ); if ( x > max ) max = x; )
+	REPEAT_TIMED( "pop_pair", N, pair(short, char) x = pop( tp ); if ( x > max ) max = x; )
 }
