Index: doc/papers/general/Paper.tex
===================================================================
--- doc/papers/general/Paper.tex	(revision 732357362caa4a5fd1565cff6758e1e1608d6f47)
+++ doc/papers/general/Paper.tex	(revision 5f95b5f4ad5b5cb1706c61b047264b342ceaaaa8)
@@ -39,7 +39,10 @@
 \newcommand{\TODO}[1]{\textbf{TODO}: {\itshape #1}} % TODO included
 %\newcommand{\TODO}[1]{} % TODO elided
+
 % Default underscore is too low and wide. Cannot use lstlisting "literate" as replacing underscore
-% removes it as a variable-name character so keyworks in variables are highlighted
-\DeclareTextCommandDefault{\textunderscore}{\leavevmode\makebox[1.2ex][c]{\rule{1ex}{0.1ex}}}
+% removes it as a variable-name character so keywords in variables are highlighted. MUST APPEAR
+% AFTER HYPERREF.
+%\DeclareTextCommandDefault{\textunderscore}{\leavevmode\makebox[1.2ex][c]{\rule{1ex}{0.1ex}}}
+\renewcommand{\textunderscore}{\leavevmode\makebox[1.2ex][c]{\rule{1ex}{0.075ex}}}
 
 \makeatletter
@@ -49,30 +52,50 @@
 \setlength{\parindentlnth}{\parindent}
 
+\newcommand{\LstKeywordStyle}[1]{{\lst@basicstyle{\lst@keywordstyle{#1}}}}
+\newcommand{\LstCommentStyle}[1]{{\lst@basicstyle{\lst@commentstyle{#1}}}}
+
 \newlength{\gcolumnposn}				% temporary hack because lstlisting does not handle tabs correctly
 \newlength{\columnposn}
 \setlength{\gcolumnposn}{2.75in}
 \setlength{\columnposn}{\gcolumnposn}
-\newcommand{\C}[2][\@empty]{\ifx#1\@empty\else\global\setlength{\columnposn}{#1}\global\columnposn=\columnposn\fi\hfill\makebox[\textwidth-\columnposn][l]{\lst@commentstyle{#2}}}
+\newcommand{\C}[2][\@empty]{\ifx#1\@empty\else\global\setlength{\columnposn}{#1}\global\columnposn=\columnposn\fi\hfill\makebox[\textwidth-\columnposn][l]{\lst@basicstyle{\LstCommentStyle{#2}}}}
 \newcommand{\CRT}{\global\columnposn=\gcolumnposn}
+
+% Denote newterms in particular font and index them without particular font and in lowercase, e.g., \newterm{abc}.
+% The option parameter provides an index term different from the new term, e.g., \newterm[\texttt{abc}]{abc}
+% The star version does not lowercase the index information, e.g., \newterm*{IBM}.
+\newcommand{\newtermFontInline}{\emph}
+\newcommand{\newterm}{\@ifstar\@snewterm\@newterm}
+\newcommand{\@newterm}[2][\@empty]{\lowercase{\def\temp{#2}}{\newtermFontInline{#2}}\ifx#1\@empty\index{\temp}\else\index{#1@{\protect#2}}\fi}
+\newcommand{\@snewterm}[2][\@empty]{{\newtermFontInline{#2}}\ifx#1\@empty\index{#2}\else\index{#1@{\protect#2}}\fi}
 
 % Latin abbreviation
 \newcommand{\abbrevFont}{\textit}	% set empty for no italics
+\newcommand{\EG}{\abbrevFont{e}.\abbrevFont{g}.}
 \newcommand*{\eg}{%
-	\@ifnextchar{,}{\abbrevFont{e}.\abbrevFont{g}.}%
-		{\@ifnextchar{:}{\abbrevFont{e}.\abbrevFont{g}.}%
-			{\abbrevFont{e}.\abbrevFont{g}.,\xspace}}%
+	\@ifnextchar{,}{\EG}%
+		{\@ifnextchar{:}{\EG}%
+			{\EG,\xspace}}%
 }%
+\newcommand{\IE}{\abbrevFont{i}.\abbrevFont{e}.}
 \newcommand*{\ie}{%
-	\@ifnextchar{,}{\abbrevFont{i}.\abbrevFont{e}.}%
-		{\@ifnextchar{:}{\abbrevFont{i}.\abbrevFont{e}.}%
-			{\abbrevFont{i}.\abbrevFont{e}.,\xspace}}%
+	\@ifnextchar{,}{\IE}%
+		{\@ifnextchar{:}{\IE}%
+			{\IE,\xspace}}%
 }%
+\newcommand{\ETC}{\abbrevFont{etc}}
 \newcommand*{\etc}{%
-	\@ifnextchar{.}{\abbrevFont{etc}}%
-        {\abbrevFont{etc}.\xspace}%
+	\@ifnextchar{.}{\ETC}%
+        {\ETC\xspace}%
 }%
-\newcommand{\etal}{%
-	\@ifnextchar{.}{\abbrevFont{et~al}}%
-	        {\abbrevFont{et al}.\xspace}%
+\newcommand{\ETAL}{\abbrevFont{et}\hspace{2pt}\abbrevFont{al}}
+\newcommand*{\etal}{%
+	\@ifnextchar{.}{\protect\ETAL}%
+		{\abbrevFont{\protect\ETAL}.\xspace}%
+}%
+\newcommand{\VIZ}{\abbrevFont{viz}}
+\newcommand*{\viz}{%
+	\@ifnextchar{.}{\VIZ}%
+		{\abbrevFont{\VIZ}.\xspace}%
 }%
 \makeatother
@@ -80,8 +103,12 @@
 % CFA programming language, based on ANSI C (with some gcc additions)
 \lstdefinelanguage{CFA}[ANSI]{C}{
-	morekeywords={_Alignas,_Alignof,__alignof,__alignof__,asm,__asm,__asm__,_At,_Atomic,__attribute,__attribute__,auto,
-		_Bool,catch,catchResume,choose,_Complex,__complex,__complex__,__const,__const__,disable,dtype,enable,__extension__,
-		fallthrough,fallthru,finally,forall,ftype,_Generic,_Imaginary,inline,__label__,lvalue,_Noreturn,one_t,otype,restrict,_Static_assert,
-		_Thread_local,throw,throwResume,trait,try,ttype,typeof,__typeof,__typeof__,zero_t},
+	morekeywords={
+		_Alignas, _Alignof, __alignof, __alignof__, asm, __asm, __asm__, _At, __attribute,
+		__attribute__, auto, _Bool, catch, catchResume, choose, _Complex, __complex, __complex__,
+		__const, __const__, disable, dtype, enable, __extension__, fallthrough, fallthru,
+		finally, forall, ftype, _Generic, _Imaginary, inline, __label__, lvalue, _Noreturn, one_t,
+		otype, restrict, _Static_assert, throw, throwResume, trait, try, ttype, typeof, __typeof,
+		__typeof__, virtual, with, zero_t},
+	moredirectives={defined,include_next}%
 }%
 
@@ -91,5 +118,5 @@
 basicstyle=\linespread{0.9}\sf,							% reduce line spacing and use sanserif font
 stringstyle=\tt,										% use typewriter font
-tabsize=4,												% 4 space tabbing
+tabsize=5,												% N space tabbing
 xleftmargin=\parindentlnth,								% indent code to paragraph indentation
 %mathescape=true,										% LaTeX math escape in CFA code $...$
@@ -101,7 +128,7 @@
 belowskip=3pt,
 % replace/adjust listing characters that look bad in sanserif
-literate={-}{\makebox[1.4ex][c]{\raisebox{0.5ex}{\rule{1.2ex}{0.06ex}}}}1 {^}{\raisebox{0.6ex}{$\scriptscriptstyle\land\,$}}1
+literate={-}{\makebox[1ex][c]{\raisebox{0.4ex}{\rule{0.8ex}{0.1ex}}}}1 {^}{\raisebox{0.6ex}{$\scriptscriptstyle\land\,$}}1
 	{~}{\raisebox{0.3ex}{$\scriptstyle\sim\,$}}1 % {`}{\ttfamily\upshape\hspace*{-0.1ex}`}1
-	{<-}{$\leftarrow$}2 {=>}{$\Rightarrow$}2 {->}{\makebox[1.4ex][c]{\raisebox{0.5ex}{\rule{1.2ex}{0.06ex}}}\kern-0.3ex\textgreater}2,
+	{<-}{$\leftarrow$}2 {=>}{$\Rightarrow$}2 {->}{\makebox[1ex][c]{\raisebox{0.4ex}{\rule{0.8ex}{0.075ex}}}\kern-0.2ex\textgreater}2,
 moredelim=**[is][\color{red}]{`}{`},
 }% lstset
@@ -109,4 +136,12 @@
 % inline code @...@
 \lstMakeShortInline@%
+
+\lstnewenvironment{cfa}[1][]
+{\lstset{#1}}
+{}
+\lstnewenvironment{C++}[1][]                            % use C++ style
+{\lstset{language=C++,moredelim=**[is][\protect\color{red}]{`}{`},#1}\lstset{#1}}
+{}
+
 
 \title{Generic and Tuple Types with Efficient Dynamic Layout in \protect\CFA}
@@ -148,5 +183,5 @@
 The C programming language is a foundational technology for modern computing with millions of lines of code implementing everything from commercial operating-systems to hobby projects.
 This installation base and the programmers producing it represent a massive software-engineering investment spanning decades and likely to continue for decades more.
-The \cite{TIOBE} ranks the top 5 most popular programming languages as: Java 16\%, \Textbf{C 7\%}, \Textbf{\CC 5\%}, \Csharp 4\%, Python 4\% = 36\%, where the next 50 languages are less than 3\% each with a long tail.
+The TIOBE~\cite{TIOBE} ranks the top 5 most popular programming languages as: Java 16\%, \Textbf{C 7\%}, \Textbf{\CC 5\%}, \Csharp 4\%, Python 4\% = 36\%, where the next 50 languages are less than 3\% each with a long tail.
 The top 3 rankings over the past 30 years are:
 \lstDeleteShortInline@%
@@ -185,5 +220,5 @@
 \label{sec:poly-fns}
 
-\CFA{}\hspace{1pt}'s polymorphism was originally formalized by \cite{Ditchfield92}, and first implemented by \cite{Bilson03}.
+\CFA{}\hspace{1pt}'s polymorphism was originally formalized by Ditchfield~\cite{Ditchfield92}, and first implemented by Bilson~\cite{Bilson03}.
 The signature feature of \CFA is parametric-polymorphic functions~\cite{forceone:impl,Cormack90,Duggan96} with functions generalized using a @forall@ clause (giving the language its name):
 \begin{lstlisting}
@@ -258,5 +293,5 @@
 }
 \end{lstlisting}
-Within the block, the nested version of @<@ performs @>@ and this local version overrides the built-in @<@ so it is passed to @qsort@.
+Within the block, the nested version of @?<?@ performs @?>?@ and this local version overrides the built-in @?<?@ so it is passed to @qsort@.
 Hence, programmers can easily form local environments, adding and modifying appropriate functions, to maximize reuse of other existing functions and types.
 
@@ -544,5 +579,5 @@
 p`->0` = 5;									$\C{// change quotient}$
 bar( qr`.1`, qr );							$\C{// pass remainder and quotient/remainder}$
-rem = [42, div( 13, 5 )]`.0.1`;				$\C{// access 2nd component of 1st component of tuple expression}$
+rem = [div( 13, 5 ), 42]`.0.1`;				$\C{// access 2nd component of 1st component of tuple expression}$
 \end{lstlisting}
 
@@ -730,5 +765,5 @@
 \end{lstlisting}
 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~\cite{Bilson03}.
+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{lstlisting}
@@ -902,4 +937,373 @@
 
 
+\section{Control Structures}
+
+
+\subsection{\texorpdfstring{Labelled \LstKeywordStyle{continue} / \LstKeywordStyle{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.
+Unfortunately, this restriction forces programmers to use @goto@ to achieve the equivalent control-flow for more than one level of nesting.
+To prevent having to switch to the @goto@, \CFA extends the @continue@ and @break@ with a target label to support static multi-level exit~\cite{Buhr85}, as in Java.
+For both @continue@ and @break@, the target label must be directly associated with a @for@, @while@ or @do@ statement;
+for @break@, the target label can also be associated with a @switch@, @if@ or compound (@{}@) statement.
+Figure~\ref{f:MultiLevelExit} shows @continue@ and @break@ indicating the specific control structure, and the corresponding C program using only @goto@ and labels.
+The innermost loop has 7 exit points, which cause continuation or termination of one or more of the 7 nested control-structures.
+
+\begin{figure}
+\lstDeleteShortInline@%
+\begin{tabular}{@{\hspace{\parindentlnth}}l@{\hspace{\parindentlnth}}l@{\hspace{\parindentlnth}}l@{}}
+\multicolumn{1}{@{\hspace{\parindentlnth}}c@{\hspace{\parindentlnth}}}{\textbf{\CFA}}	& \multicolumn{1}{@{\hspace{\parindentlnth}}c}{\textbf{C}}	\\
+\begin{cfa}
+`LC:` {
+	... $declarations$ ...
+	`LS:` switch ( ... ) {
+	  case 3:
+		`LIF:` if ( ... ) {
+			`LF:` for ( ... ) {
+				`LW:` while ( ... ) {
+					... break `LC`; ...
+					... break `LS`; ...
+					... break `LIF`; ...
+					... continue `LF;` ...
+					... break `LF`; ...
+					... continue `LW`; ...
+					... break `LW`; ...
+				} // while
+			} // for
+		} else {
+			... break `LIF`; ...
+		} // if
+	} // switch
+} // compound
+\end{cfa}
+&
+\begin{cfa}
+{
+	... $declarations$ ...
+	switch ( ... ) {
+	  case 3:
+		if ( ... ) {
+			for ( ... ) {
+				while ( ... ) {
+					... goto `LC`; ...
+					... goto `LS`; ...
+					... goto `LIF`; ...
+					... goto `LFC`; ...
+					... goto `LFB`; ...
+					... goto `LWC`; ...
+					... goto `LWB`; ...
+				  `LWC`: ; } `LWB:` ;
+			  `LFC:` ; } `LFB:` ;
+		} else {
+			... goto `LIF`; ...
+		} `L3:` ;
+	} `LS:` ;
+} `LC:` ;
+\end{cfa}
+&
+\begin{cfa}
+
+
+
+
+
+
+
+// terminate compound
+// terminate switch
+// terminate if
+// continue loop
+// terminate loop
+// continue loop
+// terminate loop
+
+
+
+// terminate if
+
+
+
+\end{cfa}
+\end{tabular}
+\lstMakeShortInline@%
+\caption{Multi-level Exit}
+\label{f:MultiLevelExit}
+\end{figure}
+
+Both labelled @continue@ and @break@ are a @goto@ restricted in the following ways:
+\begin{itemize}
+\item
+They cannot create a loop, which means only the looping constructs cause looping.
+This restriction means all situations resulting in repeated execution are clearly delineated.
+\item
+They cannot branch into a control structure.
+This restriction prevents missing declarations and/or initializations at the start of a control structure resulting in undefined behaviour.
+\end{itemize}
+The advantage of the labelled @continue@/@break@ is allowing static multi-level exits without having to use the @goto@ statement, and tying control flow to the target control structure rather than an arbitrary point in a program.
+Furthermore, the location of the label at the \emph{beginning} of the target control structure informs the reader (eye candy) that complex control-flow is occurring in the body of the control structure.
+With @goto@, the label is at the end of the control structure, which fails to convey this important clue early enough to the reader.
+Finally, using an explicit target for the transfer instead of an implicit target allows new constructs to be added or removed without affecting existing constructs.
+The implicit targets of the current @continue@ and @break@, \ie the closest enclosing loop or @switch@, change as certain constructs are added or removed.
+
+\TODO{choose and fallthrough here as well?}
+
+
+\subsection{\texorpdfstring{\LstKeywordStyle{with} Clause / Statement}{with Clause / Statement}}
+\label{s:WithClauseStatement}
+
+Grouping heterogenous data into \newterm{aggregate}s is a common programming practice, and an aggregate can be further organized into more complex structures, such as arrays and containers:
+\begin{cfa}
+struct S {								$\C{// aggregate}$
+	char c;								$\C{// fields}$
+	int i;
+	double d;
+};
+S s, as[10];
+\end{cfa}
+However, routines manipulating aggregates have repeition of the aggregate name to access its containing fields:
+\begin{cfa}
+void f( S s ) {
+	`s.`c; `s.`i; `s.`d;				$\C{// access containing fields}$
+}
+\end{cfa}
+A similar situation occurs in object-oriented programming, \eg \CC:
+\begin{C++}
+class C {
+	char c;								$\C{// fields}$
+	int i;
+	double d;
+	int mem() {							$\C{// implicit "this" parameter}$
+		`this->`c; `this->`i; `this->`d;$\C{// access containing fields}$
+	}
+}
+\end{C++}
+Nesting of member routines in a \lstinline[language=C++]@class@ allows eliding \lstinline[language=C++]@this->@ because of nested lexical-scoping.
+
+% In object-oriented programming, there is an implicit first parameter, often names @self@ or @this@, which is elided.
+% In any programming language, some functions have a naturally close relationship with a particular data type. 
+% Object-oriented programming allows this close relationship to be codified in the language by making such functions \emph{class methods} of their related data type.
+% Class methods have certain privileges with respect to their associated data type, notably un-prefixed access to the fields of that data type. 
+% When writing C functions in an object-oriented style, this un-prefixed access is swiftly missed, as access to fields of a @Foo* f@ requires an extra three characters @f->@ every time, which disrupts coding flow and clutters the produced code. 
+% 
+% \TODO{Fill out section. Be sure to mention arbitrary expressions in with-blocks, recent change driven by Thierry to prioritize field name over parameters.}
+
+\CFA provides a @with@ clause/statement (see Pascal~\cite[\S~4.F]{Pascal}) to elided aggregate qualification to fields by opening a scope containing field identifiers.
+Hence, the qualified fields become variables, and making it easier to optimizing field references in a block.
+\begin{cfa}
+void f( S s ) `with s` {				$\C{// with clause}$
+	c; i; d;							$\C{\color{red}// s.c, s.i, s.d}$
+}
+\end{cfa}
+and the equivalence for object-style programming is:
+\begin{cfa}
+int mem( S & this ) `with this` {		$\C{// with clause}$
+	c; i; d;							$\C{\color{red}// this.c, this.i, this.d}$
+}
+\end{cfa}
+The key generality over the object-oriented approach is that one aggregate parameter \lstinline[language=C++]@this@ is not treated specially over other aggregate parameters:
+\begin{cfa}
+struct T { double m, n; };
+int mem( S & s, T & t ) `with s, t` {	$\C{// multiple aggregate parameters}$
+	c; i; d;							$\C{\color{red}// s.c, s.i, s.d}$
+	m; n;								$\C{\color{red}// t.m, t.n}$
+}
+\end{cfa}
+The equivalent object-oriented style is:
+\begin{cfa}
+int S::mem( T & t ) {					$\C{// multiple aggregate parameters}$
+	c; i; d;							$\C{\color{red}// this-\textgreater.c, this-\textgreater.i, this-\textgreater.d}$
+	`t.`m; `t.`n;
+}
+\end{cfa}
+
+The statement form is used within a block:
+\begin{cfa}
+int foo() {
+	struct S1 { ... } s1;
+	struct S2 { ... } s2;
+	`with s1` {						$\C{// with statement}$
+		// access fields of s1 without qualification
+		`with s2` {					$\C{// nesting}$
+			// access fields of s1 and s2 without qualification
+		}
+	}
+	`with s1, s2` {
+		// access unambiguous fields of s1 and s2 without qualification
+	}
+}
+\end{cfa}
+
+When opening multiple structures, fields with the same name and type are ambiguous and must be fully qualified.
+For fields with the same name but different type, context/cast can be used to disambiguate.
+\begin{cfa}
+struct S { int i; int j; double m; } a, c;
+struct T { int i; int k; int m } b, c;
+`with a, b` {
+	j + k;							$\C{// unambiguous, unique names define unique types}$
+	i;								$\C{// ambiguous, same name and type}$
+	a.i + b.i;						$\C{// unambiguous, qualification defines unique names}$
+	m;								$\C{// ambiguous, same name and no context to define unique type}$
+	m = 5.0;						$\C{// unambiguous, same name and context defines unique type}$
+	m = 1;							$\C{// unambiguous, same name and context defines unique type}$
+}
+`with c` { ... }					$\C{// ambiguous, same name and no context}$
+`with (S)c` { ... }					$\C{// unambiguous, same name and cast defines unique type}$
+\end{cfa}
+
+The components in the "with" clause
+
+  with a, b, c { ... }
+
+serve 2 purposes: each component provides a type and object. The type must be a
+structure type. Enumerations are already opened, and I think a union is opened
+to some extent, too. (Or is that just unnamed unions?) The object is the target
+that the naked structure-fields apply to. The components are open in "parallel"
+at the scope of the "with" clause/statement, so opening "a" does not affect
+opening "b", etc. This semantic is different from Pascal, which nests the
+openings.
+
+Having said the above, it seems reasonable to allow a "with" component to be an
+expression. The type is the static expression-type and the object is the result
+of the expression. Again, the type must be an aggregate. Expressions require
+parenthesis around the components.
+
+  with( a, b, c ) { ... }
+
+Does this now make sense?
+
+Having written more CFA code, it is becoming clear to me that I *really* want
+the "with" to be implemented because I hate having to type all those object
+names for fields. It's a great way to drive people away from the language.
+
+
+\subsection{Exception Handling ???}
+
+
+\section{Declarations}
+
+It is important to the design team that \CFA subjectively ``feel like'' C to user programmers. 
+An important part of this subjective feel is maintaining C's procedural programming paradigm, as opposed to the object-oriented paradigm of other systems languages such as \CC and Rust. 
+Maintaining this procedural paradigm means that coding patterns that work in C will remain not only functional but idiomatic in \CFA, reducing the mental burden of retraining C programmers and switching between C and \CFA development. 
+Nonetheless, some features of object-oriented languages are undeniably convienient, and the \CFA design team has attempted to adapt them to a procedural paradigm so as to incorporate their benefits into \CFA; two of these features are resource management and name scoping.
+
+
+\subsection{Alternative Declaration Syntax}
+
+
+\subsection{References}
+
+All variables in C have an \emph{address}, a \emph{value}, and a \emph{type}; at the position in the program's memory denoted by the address, there exists a sequence of bits (the value), with the length and semantic meaning of this bit sequence defined by the type. 
+The C type system does not always track the relationship between a value and its address; a value that does not have a corresponding address is called a \emph{rvalue} (for ``right-hand value''), while a value that does have an address is called a \emph{lvalue} (for ``left-hand value''); in @int x; x = 42;@ the variable expression @x@ on the left-hand-side of the assignment is a lvalue, while the constant expression @42@ on the right-hand-side of the assignment is a rvalue.
+Which address a value is located at is sometimes significant; the imperative programming paradigm of C relies on the mutation of values at specific addresses. 
+Within a lexical scope, lvalue exressions can be used in either their \emph{address interpretation} to determine where a mutated value should be stored or in their \emph{value interpretation} to refer to their stored value; in @x = y;@ in @{ int x, y = 7; x = y; }@, @x@ is used in its address interpretation, while y is used in its value interpretation.
+Though this duality of interpretation is useful, C lacks a direct mechanism to pass lvalues between contexts, instead relying on \emph{pointer types} to serve a similar purpose. 
+In C, for any type @T@ there is a pointer type @T*@, the value of which is the address of a value of type @T@; a pointer rvalue can be explicitly \emph{dereferenced} to the pointed-to lvalue with the dereference operator @*?@, while the rvalue representing the address of a lvalue can be obtained with the address-of operator @&?@.
+
+\begin{cfa}
+int x = 1, y = 2, * p1, * p2, ** p3;
+p1 = &x;  $\C{// p1 points to x}$
+p2 = &y;  $\C{// p2 points to y}$
+p3 = &p1;  $\C{// p3 points to p1}$
+\end{cfa}
+
+Unfortunately, the dereference and address-of operators introduce a great deal of syntactic noise when dealing with pointed-to values rather than pointers, as well as the potential for subtle bugs. 
+It would be desirable to have the compiler figure out how to elide the dereference operators in a complex expression such as @*p2 = ((*p1 + *p2) * (**p3 - *p1)) / (**p3 - 15);@, for both brevity and clarity.
+However, since C defines a number of forms of \emph{pointer arithmetic}, two similar expressions involving pointers to arithmetic types (\eg @*p1 + x@ and @p1 + x@) may each have well-defined but distinct semantics, introducing the possibility that a user programmer may write one when they mean the other, and precluding any simple algorithm for elision of dereference operators.
+To solve these problems, \CFA introduces reference types @T&@; a @T&@ has exactly the same value as a @T*@, but where the @T*@ takes the address interpretation by default, a @T&@ takes the value interpretation by default, as below:
+
+\begin{cfa}
+inx x = 1, y = 2, & r1, & r2, && r3;
+&r1 = &x;  $\C{// r1 points to x}$
+&r2 = &y;  $\C{// r2 points to y}$
+&&r3 = &&r1;  $\C{// r3 points to r2}$
+r2 = ((r1 + r2) * (r3 - r1)) / (r3 - 15);  $\C{// implicit dereferencing}$
+\end{cfa}
+
+Except for auto-dereferencing by the compiler, this reference example is exactly the same as the previous pointer example. 
+Hence, a reference behaves like a variable name -- an lvalue expression which is interpreted as a value, but also has the type system track the address of that value. 
+One way to conceptualize a reference is via a rewrite rule, where the compiler inserts a dereference operator before the reference variable for each reference qualifier in the reference variable declaration, so the previous example implicitly acts like:
+
+\begin{cfa}
+`*`r2 = ((`*`r1 + `*`r2) * (`**`r3 - `*`r1)) / (`**`r3 - 15);
+\end{cfa}
+
+References in \CFA are similar to those in \CC, but with a couple important improvements, both of which can be seen in the example above. 
+Firstly, \CFA does not forbid references to references, unlike \CC. 
+This provides a much more orthogonal design for library implementors, obviating the need for workarounds such as @std::reference_wrapper@. 
+
+Secondly, unlike the references in \CC which always point to a fixed address, \CFA references are rebindable. 
+This allows \CFA references to be default-initialized (to a null pointer), and also to point to different addresses throughout their lifetime. 
+This rebinding is accomplished without adding any new syntax to \CFA, but simply by extending the existing semantics of the address-of operator in C. 
+In C, the address of a lvalue is always a rvalue, as in general that address is not stored anywhere in memory, and does not itself have an address. 
+In \CFA, the address of a @T&@ is a lvalue @T*@, as the address of the underlying @T@ is stored in the reference, and can thus be mutated there. 
+The result of this rule is that any reference can be rebound using the existing pointer assignment semantics by assigning a compatible pointer into the address of the reference, \eg @&r1 = &x;@ above. 
+This rebinding can occur to an arbitrary depth of reference nesting; $n$ address-of operators applied to a reference nested $m$ times will produce an lvalue pointer nested $n$ times if $n \le m$ (note that $n = m+1$ is simply the usual C rvalue address-of operator applied to the $n = m$ case).
+The explicit address-of operators can be thought of as ``cancelling out'' the implicit dereference operators, \eg @(&`*`)r1 = &x;@ or @(&(&`*`)`*`)r3 = &(&`*`)r1;@ or even @(&`*`)r2 = (&`*`)`*`r3;@ for @&r2 = &r3;@.
+
+Since pointers and references share the same internal representation, code using either is equally performant; in fact the \CFA compiler converts references to pointers internally, and the choice between them in user code can be made based solely on convenience. 
+By analogy to pointers, \CFA references also allow cv-qualifiers:
+
+\begin{cfa}
+const int cx = 5;		$\C{// cannot change cx}$
+const int & cr = cx;	$\C{// cannot change cr's referred value}$
+&cr = &cx;				$\C{// rebinding cr allowed}$
+cr = 7;					$\C{// ERROR, cannot change cr}$
+int & const rc = x;		$\C{// must be initialized, like in \CC}$
+&rc = &x;				$\C{// ERROR, cannot rebind rc}$
+rc = 7;					$\C{// x now equal to 7}$
+\end{cfa}
+
+\TODO{Pull more draft text from user manual; make sure to discuss initialization and reference conversions}
+
+
+\subsection{Constructors and Destructors}
+
+One of the strengths of C is the control over memory management it gives programmers, allowing resource release to be more consistent and precisely timed than is possible with garbage-collected memory management. 
+However, this manual approach to memory management is often verbose, and it is useful to manage resources other than memory (\eg file handles) using the same mechanism as memory. 
+\CC is well-known for an approach to manual memory management that addresses both these issues, Resource Allocation Is Initialization (RAII), implemented by means of special \emph{constructor} and \emph{destructor} functions; we have implemented a similar feature in \CFA.
+
+\TODO{Fill out section. Mention field-constructors and at-equal escape hatch to C-style initialization. Probably pull some text from Rob's thesis for first draft.}
+
+
+\subsection{Default Parameters}
+
+
+\section{Literals}
+
+
+\subsection{0/1}
+
+\TODO{Some text already at the end of Section~\ref{sec:poly-fns}}
+
+
+\subsection{Units}
+
+Alternative call syntax (literal argument before routine name) to convert basic literals into user literals.
+
+{\lstset{language=CFA,deletedelim=**[is][]{`}{`},moredelim=**[is][\color{red}]{@}{@}}
+\begin{cfa}
+struct Weight { double stones; };
+
+void ?{}( Weight & w ) { w.stones = 0; } $\C{// operations}$
+void ?{}( Weight & w, double w ) { w.stones = w; }
+Weight ?+?( Weight l, Weight r ) { return (Weight){ l.stones + r.stones }; }
+
+Weight @?`st@( double w ) { return (Weight){ w }; } $\C{// backquote for units}$
+Weight @?`lb@( double w ) { return (Weight){ w / 14.0 }; }
+Weight @?`kg@( double w ) { return (Weight) { w * 0.1575}; }
+
+int main() {
+	Weight w, hw = { 14 };			$\C{// 14 stone}$
+	w = 11@`st@ + 1@`lb@;
+	w = 70.3@`kg@;
+	w = 155@`lb@;
+	w = 0x_9b_u@`lb@;				$\C{// hexadecimal unsigned weight (155)}$
+	w = 0_233@`lb@;					$\C{// octal weight (155)}$
+	w = 5@`st@ + 8@`kg@ + 25@`lb@ + hw;
+}
+\end{cfa}
+}%
+
+
 \section{Evaluation}
 \label{sec:eval}
@@ -1013,5 +1417,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~\cite{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 concepts~\cite{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.
 
@@ -1021,17 +1425,17 @@
 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.
-\cite{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 structure types, and so is not a practical C replacement.
-
-\cite{obj-c-book} is an industrially successful extension to C.
+Smith and Volpano~\cite{Smith98} present Polymorphic C, an ML dialect with polymorphic functions, C-like syntax, and pointer types; it lacks many of C's features, however, most notably structure types, and so is not a practical C replacement.
+
+Objective-C~\cite{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 \cite{xcode7}, historically using less-efficient runtime checking of object types.
-The~\cite{GObject} framework also adds object-oriented programming with runtime type-checking and reference-counting garbage-collection to C;
+The GObject~\cite{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.
-\cite{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.
+Vala~\cite{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~\cite{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.
 
-D~\cite{D}, Go, and~\cite{Rust} are modern, compiled languages with abstraction features similar to \CFA traits, \emph{interfaces} in D and Go and \emph{traits} in Rust.
+D~\cite{D}, Go, and Rust~\cite{Rust} are modern, compiled languages with abstraction features similar to \CFA traits, \emph{interfaces} in D and Go and \emph{traits} in Rust.
 However, each language represents a significant departure from C in terms of language model, and none has the same level of compatibility with C as \CFA.
 D and Go are garbage-collected languages, imposing the associated runtime overhead.
@@ -1054,5 +1458,5 @@
 \CCeleven introduced @std::tuple@ as a library variadic template structure.
 Tuples are a generalization of @std::pair@, in that they allow for arbitrary length, fixed-size aggregation of heterogeneous values.
-Operations include @std::get<N>@ to extract vales, @std::tie@ to create a tuple of references used for assignment, and lexicographic comparisons.
+Operations include @std::get<N>@ to extract values, @std::tie@ to create a tuple of references used for assignment, and lexicographic comparisons.
 \CCseventeen proposes \emph{structured bindings}~\cite{Sutter15} to eliminate pre-declaring variables and use of @std::tie@ for binding the results.
 This extension requires the use of @auto@ to infer the types of the new variables, so complicated expressions with a non-obvious type must be documented with some other mechanism.
@@ -1068,5 +1472,5 @@
 The goal of \CFA is to provide an evolutionary pathway for large C development-environments to be more productive and safer, while respecting the talent and skill of C programmers.
 While other programming languages purport to be a better C, they are in fact new and interesting languages in their own right, but not C extensions.
-The purpose of this paper is to introduce \CFA, and showcase two language features that illustrate the \CFA type-system and approaches taken to achieve the goal of evolutionary C extension.
+The purpose of this paper is to introduce \CFA, and showcase language features that illustrate the \CFA type-system and approaches taken to achieve the goal of evolutionary C extension.
 The contributions are a powerful type-system using parametric polymorphism and overloading, generic types, and tuples, which all have complex interactions.
 The work is a challenging design, engineering, and implementation exercise.
Index: doc/working/assertion_resolution.md
===================================================================
--- doc/working/assertion_resolution.md	(revision 5f95b5f4ad5b5cb1706c61b047264b342ceaaaa8)
+++ doc/working/assertion_resolution.md	(revision 5f95b5f4ad5b5cb1706c61b047264b342ceaaaa8)
@@ -0,0 +1,62 @@
+The prototype system uses a 5-tuple for expression cost:
+1. *unsafe*: unsafe conversion cost
+2. *poly*: count of parameters and return types bound to a polymorphic type
+3. *vars*: count of polymorphic type variables
+4. -*spec*: count of polymorphic type specializations and type assertions, lowers cost
+   * e.g. given `dtype T` `T*` has spec 1, `T**` has spec 2, and each type assertion also has spec 1
+5. *safe*: safe conversion cost
+
+Note that in this framework, type assertions are bound to their unique minimum-cost resolution (if extant), but unlike the CFA'03, the cost of type assertion resolution does not change the cost of the overall expression resolution. In particular, it is possible to defer type assertion resolution arbitrarily late in expression resolution without changing the cost of any interpretation that has satisfiable type assertions. This means that we can defer assertion resolution until all the expressions explicitly provided in the user code ("primary expressions") are tentatively resolved.
+
+Even after resolving all the primary expressions, there may be types in the assertions which remain polymorphic. I will call these "auxiliary types", as in the following example (drawn from the `multi_type` test in the prototype repository):
+
+```
+struct a {};
+struct b {};
+
+forall(dtype A, dtype B | { B foo(A); A bar(B); })
+A baz(A);
+
+b foo(a);
+a bar(b);
+
+a x;
+baz(x);
+```
+
+In the course of resolving this expression, `A` is obviously bound to `a`, but `B` is left unbound by the primary expressions, an auxiliary type. There is, however, a unique min-cost resolution for this, where `B` is bound to `b`. In the cost model of the prototype system, if there is a unique min-cost mutually-satisfying resolution for the two type assertions, the cost of resolving `baz(x)` is (0, 2, 2, -2, 0).
+
+The most-common failure case for type assertions in CFA is a set of partial specializations of auxilliary types that does not ever specialize to a concrete type, as in this example (drawn from the `exp` test in the prototype repository -- note that an equivalent to the `make` function shows up fairly often as an implicit conversion from `void*` to any other pointer type, and `ctor` and `dtor` correspond to two of the common `otype` constraints):
+
+```
+struct base {};
+forall(dtype T) struct box {};
+
+void ctor(base);
+void dtor(base);
+
+forall(dtype T | { void ctor(T); void dtor(T); })
+void ctor(box(T));
+forall(dtype T | { void ctor(T); void dtor(T); })
+void dtor(box(T));
+
+forall(dtype S | { void ctor(S); void dtor(S); })
+void f(box(S));
+
+forall(dtype Q | { void ctor(Q); void dtor(Q); })
+Q make();
+
+f( make() );
+```
+
+`make()` has a cost of (0, 1, 1, -3, 0) for any binding of `ctor` and `dtor` (spec is -2 for the constraints, -1 for the partially-specialized polymorphic type `box(Q)`). `f( make() )` then forces a binding `Q => box(S)`, with a total expression cost of (0, 2, 2, -6, 0) for any satisfying resolution of the four constraints (`ctor` and `dtor` on `Q` and `S`). The given `ctor` and `dtor` for `box(T)` will satisfy the constraints on `Q` if `S` can be satisfied, so the question is what to bind the auxiliary type `S` to: `base` would work (at zero cost), as would `box(T)` (at cost (0, 1, 1, -3, 0)), provided we can bind the auxiliary type `T`, a recursive case of exactly the same problem.
+
+Now, at this point, in either the prototype cost model or that in CFA-CC, it should be clear that `S => base` is the cheapest resolution, which should be chosen. The prototype model has the advantage that it has already calculated the cost for `S => box(T)` (assuming a satisfactory `T`), while CFA-CC would determine the cost of satisfying `T` to add to the cost of `S => box(T)`. Since `T` can be `box(box(... box(base) ...))` nested arbitrarily deeply, there are an infinite number of possible bindings, and this computation does not terminate without the imposition of a limit on depth of recursive type assertion resolution.
+
+However, given this problem, a few observations can be made. Firstly, all satisfactory bindings of auxiliary types will be concrete types -- that is, they will not include any unbound type variables. Secondly, since type assertion resolution does not allow conversions (at least in the prototype system -- there may be type conversions to match a type variable, but its assertions cannot use implicit conversions), a concrete match for an assertion parameter will always be cheaper than a polymorphic match for an assertion parameter (which may recursively add more type assertions).
+
+It follows, then, that if a mutually-satisfactory set of concrete matches for all assertion parameters can be found, that there is no cheaper set of matches including more polymorphic matches, and thus no need to attempt to recursively resolve further type assertions of potential polymorphic matches. Thus, given some set of concrete matches for all type assertions, if there is a unique min-cost such set, it can safely be used, whereas if there is no uniquely-minimal set, then the assertion set is ambiguous, as there will not be any cheaper resolution. If there is no concrete match (e.g. remove `ctor(base)` and `dtor(base)` from the example above), then the calculation may still recurse infinitely (as discussed above), however it is possible this sort of cycle could be precisely detected and terminated on, or, alternately, the existing approach of limiting depth of recursive type assertion resolution should suffice in practice.
+
+I further argue that in reasonable code the depth at which such concrete solutions can be found is likely to be fairly small, by appeal to structural-induction-based handwaving. I posit that any *useful* polymorphic function either (1) does not satisfy its own type assertions or (2) only satisfies any of its own type assertions through partial specialization of the type. `f` above would be an example of (1), while `ctor` and `dtor` would be an example of (2). `ctor` and `dtor` do satisfy their own type assertions, with the binding `T => box(T')`. However, any object that exists in the system must have a finitely-expressible type (generally with a nesting level bounded by a small natural number), so there should be very few repetitions of this cycle before an appropriate concrete type is discovered. This informal argument also applies if the cycle is composed of two or more functions which satisfy each other's type assertions. While it is syntactically and semantically legal to write a function that falls into neither category, its addition cannot make any previously-unresolvable code resolvable, and thus it is unlikely to exist in user code. An example of such a function would be this, clearly useless: `forall(dtype T | { T* f(T*); } ) T* f(T*);`
+
+In conclusion, the existing CFA-CC compiler essentially does a depth-first exploration of the space of possible resolutions of auxiliary types (up to bounded depth); a breadth-first approach would seem likely to be more efficient in practice, as it could be terminated at the first depth any solution was found with a minimal-cost solution or ambiguous result. This does not remove the necessity for an assertion recursion limit, but should prevent the compiler from reaching that limit as often in practice.
Index: src/Common/PassVisitor.impl.h
===================================================================
--- src/Common/PassVisitor.impl.h	(revision 732357362caa4a5fd1565cff6758e1e1608d6f47)
+++ src/Common/PassVisitor.impl.h	(revision 5f95b5f4ad5b5cb1706c61b047264b342ceaaaa8)
@@ -998,10 +998,18 @@
 template< typename pass_type >
 void PassVisitor< pass_type >::visit( FinallyStmt * node ) {
-	VISIT_BODY( node );
+	VISIT_START( node );
+
+	maybeAccept_impl( node->block, *this );
+
+	VISIT_END( node );
 }
 
 template< typename pass_type >
 Statement * PassVisitor< pass_type >::mutate( FinallyStmt * node ) {
-	MUTATE_BODY( Statement, node );
+	MUTATE_START( node );
+
+	maybeMutate_impl( node->block, *this );
+
+	MUTATE_END( Statement, node );
 }
 
Index: src/GenPoly/Box.cc
===================================================================
--- src/GenPoly/Box.cc	(revision 732357362caa4a5fd1565cff6758e1e1608d6f47)
+++ src/GenPoly/Box.cc	(revision 5f95b5f4ad5b5cb1706c61b047264b342ceaaaa8)
@@ -988,11 +988,11 @@
 
 		Expression *Pass1::handleIntrinsics( ApplicationExpr *appExpr ) {
-			if ( VariableExpr *varExpr = dynamic_cast< VariableExpr *>( appExpr->get_function() ) ) {
-				if ( varExpr->get_var()->get_linkage() == LinkageSpec::Intrinsic ) {
-					if ( varExpr->get_var()->get_name() == "?[?]" ) {
+			if ( VariableExpr *varExpr = dynamic_cast< VariableExpr *>( appExpr->function ) ) {
+				if ( varExpr->var->linkage == LinkageSpec::Intrinsic ) {
+					if ( varExpr->var->name == "?[?]" ) {
 						assert( appExpr->result );
 						assert( appExpr->get_args().size() == 2 );
-						Type *baseType1 = isPolyPtr( appExpr->get_args().front()->get_result(), scopeTyVars, env );
-						Type *baseType2 = isPolyPtr( appExpr->get_args().back()->get_result(), scopeTyVars, env );
+						Type *baseType1 = isPolyPtr( appExpr->args.front()->result, scopeTyVars, env );
+						Type *baseType2 = isPolyPtr( appExpr->args.back()->result, scopeTyVars, env );
 						assert( ! baseType1 || ! baseType2 ); // the arguments cannot both be polymorphic pointers
 						UntypedExpr *ret = 0;
@@ -1555,35 +1555,35 @@
 			// only mutate member expressions for polymorphic types
 			int tyDepth;
-			Type *objectType = hasPolyBase( memberExpr->get_aggregate()->get_result(), scopeTyVars, &tyDepth );
+			Type *objectType = hasPolyBase( memberExpr->aggregate->result, scopeTyVars, &tyDepth );
 			if ( ! objectType ) return memberExpr;
 			findGeneric( objectType ); // ensure layout for this type is available
 
 			// replace member expression with dynamically-computed layout expression
-			Expression *newMemberExpr = 0;
+			Expression *newMemberExpr = nullptr;
 			if ( StructInstType *structType = dynamic_cast< StructInstType* >( objectType ) ) {
 				// look up offset index
-				long i = findMember( memberExpr->get_member(), structType->get_baseStruct()->get_members() );
+				long i = findMember( memberExpr->member, structType->baseStruct->members );
 				if ( i == -1 ) return memberExpr;
 
 				// replace member expression with pointer to base plus offset
 				UntypedExpr *fieldLoc = new UntypedExpr( new NameExpr( "?+?" ) );
-				Expression * aggr = memberExpr->get_aggregate()->clone();
-				delete aggr->get_env(); // xxx - there's a problem with keeping the env for some reason, so for now just get rid of it
-				aggr->set_env( nullptr );
+				Expression * aggr = memberExpr->aggregate->clone();
+				delete aggr->env; // xxx - there's a problem with keeping the env for some reason, so for now just get rid of it
+				aggr->env = nullptr;
 				fieldLoc->get_args().push_back( aggr );
 				fieldLoc->get_args().push_back( makeOffsetIndex( objectType, i ) );
-				fieldLoc->set_result( memberExpr->get_result()->clone() );
+				fieldLoc->set_result( memberExpr->result->clone() );
 				newMemberExpr = fieldLoc;
 			} else if ( dynamic_cast< UnionInstType* >( objectType ) ) {
 				// union members are all at offset zero, so just use the aggregate expr
-				Expression * aggr = memberExpr->get_aggregate()->clone();
-				delete aggr->get_env(); // xxx - there's a problem with keeping the env for some reason, so for now just get rid of it
-				aggr->set_env( nullptr );
+				Expression * aggr = memberExpr->aggregate->clone();
+				delete aggr->env; // xxx - there's a problem with keeping the env for some reason, so for now just get rid of it
+				aggr->env= nullptr;
 				newMemberExpr = aggr;
-				newMemberExpr->set_result( memberExpr->get_result()->clone() );
+				newMemberExpr->result = memberExpr->result->clone();
 			} else return memberExpr;
 			assert( newMemberExpr );
 
-			Type *memberType = memberExpr->get_member()->get_type();
+			Type *memberType = memberExpr->member->get_type();
 			if ( ! isPolyType( memberType, scopeTyVars ) ) {
 				// Not all members of a polymorphic type are themselves of polymorphic type; in this case the member expression should be wrapped and dereferenced to form an lvalue
@@ -1598,5 +1598,5 @@
 
 		ObjectDecl *PolyGenericCalculator::makeVar( const std::string &name, Type *type, Initializer *init ) {
-			ObjectDecl *newObj = new ObjectDecl( name, Type::StorageClasses(), LinkageSpec::C, 0, type, init );
+			ObjectDecl *newObj = new ObjectDecl( name, Type::StorageClasses(), LinkageSpec::C, nullptr, type, init );
 			stmtsToAddBefore.push_back( new DeclStmt( newObj ) );
 			return newObj;
Index: src/GenPoly/InstantiateGeneric.cc
===================================================================
--- src/GenPoly/InstantiateGeneric.cc	(revision 732357362caa4a5fd1565cff6758e1e1608d6f47)
+++ src/GenPoly/InstantiateGeneric.cc	(revision 5f95b5f4ad5b5cb1706c61b047264b342ceaaaa8)
@@ -476,4 +476,5 @@
 			DeclarationWithType * field = strict_dynamic_cast< DeclarationWithType * >( member );
 			MemberExpr * ret = new MemberExpr( field, memberExpr->aggregate->clone() );
+			ResolvExpr::adjustExprType( ret->result ); // pointer decay
 			std::swap( ret->env, memberExpr->env );
 			delete memberExpr;
Index: src/ResolvExpr/AdjustExprType.cc
===================================================================
--- src/ResolvExpr/AdjustExprType.cc	(revision 732357362caa4a5fd1565cff6758e1e1608d6f47)
+++ src/ResolvExpr/AdjustExprType.cc	(revision 5f95b5f4ad5b5cb1706c61b047264b342ceaaaa8)
@@ -24,5 +24,5 @@
 	class AdjustExprType : public WithShortCircuiting {
 	  public:
-		AdjustExprType( const TypeEnvironment &env, const SymTab::Indexer &indexer );
+		AdjustExprType( const TypeEnvironment & env, const SymTab::Indexer & indexer );
 		void premutate( VoidType * ) { visit_children = false; }
 		void premutate( BasicType * ) { visit_children = false; }
@@ -45,6 +45,6 @@
 
 	  private:
-		const TypeEnvironment &env;
-		const SymTab::Indexer &indexer;
+		const TypeEnvironment & env;
+		const SymTab::Indexer & indexer;
 	};
 
@@ -53,4 +53,10 @@
 		Type *newType = type->acceptMutator( adjuster );
 		type = newType;
+	}
+
+	void adjustExprType( Type *& type ) {
+		TypeEnvironment env;
+		SymTab::Indexer indexer;
+		adjustExprType( type, env, indexer );
 	}
 
Index: src/ResolvExpr/Resolver.cc
===================================================================
--- src/ResolvExpr/Resolver.cc	(revision 732357362caa4a5fd1565cff6758e1e1608d6f47)
+++ src/ResolvExpr/Resolver.cc	(revision 5f95b5f4ad5b5cb1706c61b047264b342ceaaaa8)
@@ -280,5 +280,9 @@
 			std::list< Statement * > newStmts;
 			resolveWithExprs( functionDecl->withExprs, newStmts );
-			functionDecl->statements->kids.splice( functionDecl->statements->kids.begin(), newStmts );
+			if ( functionDecl->statements ) {
+				functionDecl->statements->kids.splice( functionDecl->statements->kids.begin(), newStmts );
+			} else {
+				assertf( functionDecl->withExprs.empty() && newStmts.empty(), "Function %s without a body has with-clause and/or generated with declarations.", functionDecl->name.c_str() );
+			}
 		}
 	}
Index: src/ResolvExpr/typeops.h
===================================================================
--- src/ResolvExpr/typeops.h	(revision 732357362caa4a5fd1565cff6758e1e1608d6f47)
+++ src/ResolvExpr/typeops.h	(revision 5f95b5f4ad5b5cb1706c61b047264b342ceaaaa8)
@@ -55,4 +55,7 @@
 	/// Replaces array types with the equivalent pointer, and function types with a pointer-to-function
 	void adjustExprType( Type *&type, const TypeEnvironment &env, const SymTab::Indexer &indexer );
+
+	/// Replaces array types with the equivalent pointer, and function types with a pointer-to-function using empty TypeEnvironment and Indexer
+	void adjustExprType( Type *& type );
 
 	template< typename ForwardIterator >
Index: src/driver/cfa.cc
===================================================================
--- src/driver/cfa.cc	(revision 732357362caa4a5fd1565cff6758e1e1608d6f47)
+++ src/driver/cfa.cc	(revision 5f95b5f4ad5b5cb1706c61b047264b342ceaaaa8)
@@ -10,6 +10,6 @@
 // Created On       : Tue Aug 20 13:44:49 2002
 // Last Modified By : Peter A. Buhr
-// Last Modified On : Thu Feb  1 22:26:10 2018
-// Update Count     : 163
+// Last Modified On : Mon Feb  5 22:05:28 2018
+// Update Count     : 166
 //
 
@@ -258,4 +258,13 @@
 		#endif
 
+		args[nargs] = "-Xlinker";
+		nargs += 1;
+		args[nargs] = "--undefined=__cfaabi_dbg_bits_write";
+		nargs += 1;
+		args[nargs] = "-Xlinker";
+		nargs += 1;
+		args[nargs] = "--undefined=__cfaabi_interpose_startup";
+		nargs += 1;
+
 		// include the cfa library in case it's needed
 		args[nargs] = "-L" CFA_LIBDIR;
@@ -273,15 +282,6 @@
 		args[nargs] = "-lrt";
 		nargs += 1;
-		args[nargs] = "-Xlinker";
-		nargs += 1;
-		args[nargs] = "--undefined=__cfaabi_dbg_bits_write";
-		nargs += 1;
-		args[nargs] = "-Xlinker";
-		nargs += 1;
-		args[nargs] = "--undefined=__cfaabi_interpose_startup";
-		nargs += 1;
-
-	} // if
-#endif //HAVE_LIBCFA
+	} // if
+#endif // HAVE_LIBCFA
 
 	// Add exception flags (unconditionally)
@@ -333,4 +333,9 @@
 		nargs += 1;
 	} // if
+
+    args[nargs] = "-Xlinker";							// used by backtrace
+    nargs += 1;
+    args[nargs] = "-export-dynamic";
+    nargs += 1;
 
 	// execute the compilation command
Index: src/libcfa/interpose.c
===================================================================
--- src/libcfa/interpose.c	(revision 732357362caa4a5fd1565cff6758e1e1608d6f47)
+++ src/libcfa/interpose.c	(revision 5f95b5f4ad5b5cb1706c61b047264b342ceaaaa8)
@@ -10,6 +10,6 @@
 // Created On       : Wed Mar 29 16:10:31 2017
 // Last Modified By : Peter A. Buhr
-// Last Modified On : Fri Jul 21 22:27:33 2017
-// Update Count     : 1
+// Last Modified On : Mon Feb  5 23:40:04 2018
+// Update Count     : 17
 //
 
@@ -32,6 +32,4 @@
 #include "bits/signal.h"
 #include "startup.h"
-
-void __cfaabi_interpose_startup(void)  __attribute__(( constructor( STARTUP_PRIORITY_CORE ) ));
 
 typedef void (*generic_fptr_t)(void);
@@ -92,13 +90,16 @@
 void sigHandler_abort( __CFA_SIGPARMS__ );
 
-void __cfaabi_interpose_startup() {
-	const char *version = NULL;
-
-	INIT_REALRTN( abort, version );
-	INIT_REALRTN( exit, version );
-
-	__kernel_sigaction( SIGSEGV, sigHandler_segv , SA_SIGINFO );      // Failure handler
-	__kernel_sigaction( SIGBUS , sigHandler_segv , SA_SIGINFO );      // Failure handler
-	__kernel_sigaction( SIGABRT, sigHandler_abort, SA_SIGINFO );      // Failure handler
+extern "C" {
+	void __cfaabi_interpose_startup(void)  __attribute__(( constructor( STARTUP_PRIORITY_CORE ) ));
+	void __cfaabi_interpose_startup( void ) {
+		const char *version = NULL;
+
+		INIT_REALRTN( abort, version );
+		INIT_REALRTN( exit, version );
+
+		__kernel_sigaction( SIGSEGV, sigHandler_segv , SA_SIGINFO ); // Failure handler
+		__kernel_sigaction( SIGBUS , sigHandler_segv , SA_SIGINFO ); // Failure handler
+		__kernel_sigaction( SIGABRT, sigHandler_abort, SA_SIGINFO ); // Failure handler
+	}
 }
 
@@ -108,9 +109,9 @@
 
 extern "C" {
-	void abort (void) __attribute__ ((__nothrow__, __leaf__, __noreturn__)) {
+	void abort( void ) __attribute__ ((__nothrow__, __leaf__, __noreturn__)) {
 		abortf( NULL );
 	}
 
-	void exit (int __status) __attribute__ ((__nothrow__, __leaf__, __noreturn__)) {
+	void exit( int __status ) __attribute__ ((__nothrow__, __leaf__, __noreturn__)) {
 		libc_exit(__status);
 	}
@@ -121,6 +122,6 @@
 }
 
-void * kernel_abort    (void) __attribute__ ((__nothrow__, __leaf__, __weak__)) { return NULL; }
-void   kernel_abort_msg(void * data, char * buffer, int size) __attribute__ ((__nothrow__, __leaf__, __weak__)) {}
+void * kernel_abort    ( void ) __attribute__ ((__nothrow__, __leaf__, __weak__)) { return NULL; }
+void   kernel_abort_msg( void * data, char * buffer, int size ) __attribute__ ((__nothrow__, __leaf__, __weak__)) {}
 
 enum { abort_text_size = 1024 };
@@ -133,5 +134,5 @@
 		int len;
 
-		if( fmt ) {
+		if ( fmt ) {
 			va_list args;
 			va_start( args, fmt );
@@ -142,5 +143,5 @@
 
 			__cfaabi_dbg_bits_write( abort_text, len );
-			__cfaabi_dbg_bits_write( "\n", 1 );
+			//__cfaabi_dbg_bits_write( "\n", 1 );
 		}
 
@@ -162,5 +163,5 @@
 	enum { Frames = 50 };
 	void * array[Frames];
-	int size = backtrace( array, Frames );
+	size_t size = backtrace( array, Frames );
 	char ** messages = backtrace_symbols( array, size );
 
@@ -176,4 +177,5 @@
 
 		for ( char *p = messages[i]; *p; ++p ) {
+			//__cfaabi_dbg_bits_print_nolock( "X %s\n", p);
 			// find parantheses and +offset
 			if ( *p == '(' ) {
