diff --git a/NEWPROPOSAL/FULLPROP.tex b/NEWPROPOSAL/FULLPROP.tex
index 60309cf9b316d902f0d6d4b7d85e351c2ef8985b..bbae4b51ac9f7c3f2b614636dfc8e2ac3081b279 100644
--- a/NEWPROPOSAL/FULLPROP.tex
+++ b/NEWPROPOSAL/FULLPROP.tex
@@ -209,6 +209,11 @@ easily run existing programs, and future programming languages automatically gai
 \paragraph{Baseline of knowledge and skills:}
 \label{sec:basel-knowl-skills}
 
+\newt{%
+  Several powerful high-level languages (HLLs) have been proposed for quantum programs, such as Quipper~\cite{Alexander-S.-Green:2013fk} and \Qsharp~\cite{qsharp}.
+  As with classical HLLs, these languages are not designed to be run directly on quantum hardware: instead, their compilers typically output quantum circuit descriptions, which are not tailored well to run on any particular hardware platform.
+}%
+
 \newt{%
   Our proposal is to develop an analogue of the LLVM compiler system, for quantum computation.
   The LLVM compiler system is a modularised collection of libraries for hardware realisation and optimisation for classical programming, providing the functionality which is expected of a well-designed modern compiler.
@@ -448,14 +453,14 @@ multiple options and to address high scientific and technological
 risks.
 } 
 
-Our proposed \newt{quantum compiler technology} is an advanced \textsc{zx}-style system
+Our proposed \newt{quantum compiler technology}, which we call the \dzxc (``\emph{deep ZX compilation}'') system, is an advanced \textsc{zx}-style system
 augmented with features needed for applications.
 The \zxcalculus occupies a place in quantum computation similar to the
 $\lambda$-calculus in classical computing: it provides a solid but
 austere theoretical foundation, without any niceties for practical
 usage. 
 \newt{%
-  We will augment this basic formal system with a second layer of
+  The \dzxc system will augment this basic formal system with a second layer of
 }%
 \emph{annotations} on the tensor graph, describing program parameters
 and architectural constraints of a specific hardware configuration.
@@ -464,7 +469,7 @@ the implementation (annotation layer) of the program, and is the key
 to achieving our goal of supporting multiple targets.
 
 \newt{%
-  Our quantum compiler system}
+  The \dzxc system}
 will retain the mature and effective formal tensor language of
 the \zxcalculus at its heart, ensuring semantic soundness, logical
 completeness \cite{Jeandel2017A-Complete-Axio,NW-2017},
@@ -507,10 +512,25 @@ state has a gflow then it supports deterministic 1-way computation
 \cite{D.E.-Browne2007Generalized-Flo}.  Annotating the graph with its
 gflow provides guidance for a rewrite strategy which produces an
 equivalent, space-optimal circuit \cite{Duncan:2010aa}.
-We propose to generalise this concept to encompass other sorts of information which would inform how to transform (i.e.,~to re-write) a generic representation of a quantum computational procedure.
-For example, we would develop a system which specifies both how to represent logical operations in a particular error correcting code, and how the operations are constrained in order to satisfy basic precautions to keep the realisation fault-tolerant (\ref{task:ECC}).
-We may then attempt to re-write procedures, to minimise the number of operations subject to the constraints described by those annotations.
-We may further elaborate such a system of annotations by a description of the constraints and the costs involved for operations within a particular hardware platform (\ref{task:runnable}).
+\newt{%
+  The \dzxc system
+}%
+would generalise this concept to encompass other sorts of information which would inform how to transform (i.e.,~to re-write) a generic representation of a quantum computational procedure.
+For example, 
+\newt{%
+  the \dzxc system could encorporate
+}%
+a system which specifies both how to represent logical operations in a particular error correcting code, and how the operations are constrained in order to satisfy basic precautions to keep the realisation fault-tolerant (\ref{task:ECC}).
+\newt{%
+  This would enable the \dzxc system
+}%
+to re-write procedures, to minimise the number of operations subject to the constraints described by those annotations.
+
+\newt{%
+  The \dzxc system would be modular, and allow for several different systems of annotations, for different hardware platforms or constraints one might impose on a computation.
+  One such system of annotations would be to describe
+}%
+the constraints and the costs involved for operations within a particular hardware platform (\ref{task:runnable}).
 %%For example, in
 % Other
 %examples of annotations might include paths in the graph corresponding
@@ -536,8 +556,11 @@ specific annotations (\ref{wp:backends}), and rewrite strategies which exploit t
 
 Concrete tensor networks have a fixed finite size, whereas algorithms
 are described in parametric fashion, \eg varying according the
-input size.  To accommodate this we introduce a second class of
-annotations to represent limited forms of iteration and recursion, yielding
+input size.
+\newt{%
+  To accommodate this, the \dzxc system would incorporate
+}%
+a second class of annotations to represent limited forms of iteration and recursion, yielding
 \newt{%
   \emph{parametric} \zx terms.}
 While the hardware-derived annotations are inferred in a bottom-up fashion, the parametric structure is produced top-down, based on the original
@@ -555,7 +578,11 @@ project~\cite{KZ:2015:aa, Kissinger2015Quantomatic:-A-}.
 \texttt{\bfseries \color{red!70!black} [apropos to refer to PyZX here?]}
 
 
-Early in the project, we will implement translations from existing
+Early in the development of
+\newt{%
+  the \dzxc system,
+}%
+we will implement translations from existing
 quantum programming languages~(\ref{task:trans1}).  These will provide
  examples and test cases, and allow comparative
 evaluation. % of the \azx system.  %We will adapt an existing compiler to generate parameterised \azx terms (\ref{task:trans2}).
@@ -624,8 +651,8 @@ various themes: the relation between \zx and other quantum computing representat
 }%
 \newt{%
   As with classical HLLs, these languages are not designed to be run directly on quantum hardware: instead, their compilers typically output quantum circuit descriptions, which are not tailored well to run on any particular hardware platform.
-  Rather than designing a new programming language, we propose a compiler system for quantum computers, which could serve as an interface between multiple different HLLs for quantum procedures, and various quantum hardware platforms.
-  This system would use the \zxcalculus as an internal representation of the procedure as it undergoes optimisations and translations to fit a particular hardware architecture.
+  Our proposed \dzxc system would represent an interface between multiple different HLLs for quantum procedures, and various quantum hardware platforms.
+  This system would use terms of the \zxcalculus as an internal representation of the procedure as it undergoes optimisations and translations to fit a particular hardware architecture.
   This representation would not be required from or exposed to the user,\footnote{This said, the \zxcalculus has proved a very useful notation for mathematical proofs.}
   but would be generated by a compiler front-end from programs written in existing high-level languages.
   Therefore it is essential to provide a robust, general framework for compilation of HLLs to \zx terms.
@@ -636,7 +663,7 @@ various themes: the relation between \zx and other quantum computing representat
 }%
 we first focus on a simple front end for the circuit language QASM~\cite{Cross2017Open-Quantum-As} in \ref{task:HHL} before moving towards more expressive HHLs.
 \newt{%
-  This will allow virtually any extant quantum HLL to interface with our quantum compiler system, albeit rather naively at first.
+  This will allow virtually any extant quantum HLL to interface with the \dzxc system, albeit rather naively at first.
 }%
 Later, we will perform concrete front-end
 experiments using more sophisticated existing HLLs in, for example
@@ -650,7 +677,7 @@ will also be made available to the community for rating and testing
 future compilers or optimisation techniques.  To encourage interaction
 from other research groups, and to support other languages,
 \newt{%
-  the interfaces and functionality for our quantum compiler system will be made public.
+  the interfaces and functionality for the \dzxc system will be made public.
 }%
 
 Proposed and existing quantum devices differ along a variety of axes.
@@ -664,12 +691,12 @@ restrictions on which qubits may interact directly.
 Primitive operations will require different amounts of time,
 different qubit implementations have different failure
 modes.\REM{noise,fidelitY}
-
+%
 Due to the novelty of our proposal, we adopt an exploratory approach with respect to back-end models.
 Initially, and in parallel, we study the circuit model (\ref{task:circuit-model}) and
 the 1-way model (\ref{task:mbqc-model}) because these models are well understood, stable, and have been extensively treated in the \zxcalculus literature. 
 \newt{%
-  These models will provide the prototypes for the use of annotations on top of \zx terms which will be used by our compiler system.
+  These models will allow us to prototype the development of hardware annotations for the \dzxc system.
   In both cases, this involves three tightly related tasks:
   \begin{enumerate}[label=(\roman*)]
   \item
@@ -685,12 +712,13 @@ This experience will inform the later work in \ref{wp:theory} and
 
 Although we will provide specific modules for the tasks described above,
 \newt{%
-  our quantum compiler system
+  the \dzxc system
 }%
 is intended to extensible, so we will also publish an open
 API and specification language to simplify the task of adding new
 architectures and error correcting schemes to the system
-(\ref{task:backendapi}). 
+(\ref{task:backendapi}).
+\texttt{\bfseries \color{red!70!black}[is this redundant to a paragraph above about \ref{task:testBench}?]}
 
 
 %% OUTDATED
diff --git a/NEWPROPOSAL/preamble.tex b/NEWPROPOSAL/preamble.tex
index b3938bc90f35ed9300fc759333d277b313933ef5..56b4c0489c8aaf3e1941f7081b11a1c9143e6c02 100644
--- a/NEWPROPOSAL/preamble.tex
+++ b/NEWPROPOSAL/preamble.tex
@@ -274,9 +274,10 @@
 
 \newcommand{\zx}{\textsc{zx}\xspace}
 \newcommand{\zxcalculus}{\textsc{zx}-calculus\xspace}
-\newcommand{\azx}{\texttt{\bfseries\color{red!70!black}[macro \textbackslash AZX occurs here]}\xspace}
+\newcommand{\azx}{\texttt{\bfseries\color{red!70!black}[do you mean \textbackslash DZXC?]}\xspace}
 \newcommand{\liquid}{\texttt{\bfseries\color{red!70!black}[do you mean \textbackslash Qsharp?]}\xspace}
 \newcommand{\Qsharp}{Q\texttt\#\xspace}
+\newcommand{\dzxc}{\texttt{DXZC}\xspace}
 
 \newcommand{\benREM}[1]{\texttt{\bfseries\color{red!70!black} [{#1}]}\xspace}