diff --git a/NEWPROPOSAL/FULLPROP.tex b/NEWPROPOSAL/FULLPROP.tex
index 46e9e289c2fdc9fb9459c9104e229a86eca0446a..edd0765c8554ef598db9a6c538514fe60e21993a 100644
--- a/NEWPROPOSAL/FULLPROP.tex
+++ b/NEWPROPOSAL/FULLPROP.tex
@@ -243,11 +243,11 @@ The calculus can be viewed both as a formal axiomatic theory of complementary ob
 The tensor network structure means that the \zxcalculus represents all quantum operations such as 
  initialisation, unitaries, measurements and discarding in a single notation. This notation is significantly 
      \begin{wrapfigure}{r}{0.75\textwidth}
-    \vspace*{-10mm}%
+    \vspace*{-8mm}%
 %    \texttt{\color{red!70!black} [Placeholder?]} \\[-5ex]
     \hspace*{-4mm}%
     \cgraph[0.7]{circuit-fig}%
-    \vspace*{-9mm}  
+    \vspace*{-11mm}  
     \end{wrapfigure}
 %\includegraphics[width=\textwidth]{figures/circuit-fig}
 more powerful and flexible than quantum circuits. \zx-based transformations between quantum circuits 
@@ -295,9 +295,11 @@ compilers for quantum software.
 \label{sec:contr-theme-addr}
 
 We specifically address the theme of \emph{Quantum Computation}.
-We develop tools to facilitate running quantum programs
-on any available quantum device.
-This will speed new quantum devices and architectures into use, and broaden the range of potential users of quantum computers.
+We develop tools for running quantum programs
+on any available quantum device and benchmarking algorithms and machines, significantly 
+enhancing the capabilities of near-term quantum computers.
+
+% speed new quantum devices and architectures into use, and broaden the range of potential users of quantum computers.
 
 \subsection{Novelty, level of ambition and foundational character}
 \label{sec:novelty-level-ambit}
@@ -310,100 +312,27 @@ This will speed new quantum devices and architectures into use, and broaden the
     methods to be used.}
 }
 
-\BREM{
-\begin{itemize}
-  \item Need to emphasise unique features in light of \liquid, which also claims compilation to hardware, circuit rewriting/optimisation, and error correction
-  \item \textbf{novel feature:} flexibility, via intermediate language
-  \item \textbf{novel feature:} formal basis (ZX-calculus, categorical semantics)
-  \item \textbf{novel feature:} multiple paradigms. Notably MBQC (both team members' expertise, and in methodology) and \textbf{lattice surgery} (high-level description of logical operations on error-corrected memories)
-  \item \textbf{foundational nature:} semantics of quantum programming languages is still very young, and already many dead ends. This project gives a unique opportunity for applications to drive theory.
-\end{itemize}
-}
-
 
 \paragraph{Novelty:}
 \label{sec:novelty}
 
-  Using the \zxcalculus to manage resources in quantum hardware is a totally new application of the \zxcalculus, and a totally new way to realise computations on quantum hardware.
-  Unlike sequences of gates, the tensor networks which are the terms of the \zxcalculus have no preordained causal structure beyond the global input and output.
-  This provides us with great flexibility with respect to time-space trade-offs, and will help to achieve optimal implementations on diverse architectures.
-Furthermore, our system allows transformations of tensor networks which cannot be expressed as equations between circuits \newt{as illustrated in the figure on the previous page}.
-  In addition to these benefits, the \zxcalculus is a sound and complete formal system for transforming quantum procedures, so that each program transformation which our compiler system would realise will be provably correct, and indeed comes with a proof of its correctness.
-  At the same time, the way that the \zxcalculus represents quantum procedures avoids the immediate dimensional explosion associated with explicit matrices, so that it will in many cases be more efficient than any other automated technique for reasoning about quantum procedures.
-
-
-\REM{This project rests on more than a decade of investigations into the
-categorical structure of quantum mechanics. This project therefore has a uniquely
-strong theoretical foundation, and provides us with
-insights unavailable to other approaches.% Repeated later
-}
-\REM{more}
-\REM{}
-
-\REM{Formal proofs of everything.  Formal basis (ZX-calculus, categorical semantics)}
-
-\REM{Pure symbolic manipulation; no dimension explosion!  (\liquid
-  handles up to 30 qubits -- aka 3 error corrected qubits!}
-
-
-\REM{
-However, as the RISC revolution in CPU design showed in the 1980s, there is no reason for
-instruction sets to be optimised for human comprehension once
-good compilers are available. \azx would provide a more
-flexible, powerful,  interface between quantum computers and the outside world.
-}
-
-\REM{
-From a formal perspective, \azx could be
-regarded as a formal semantics for quantum programming
-languages. However, unlike other existing semantics such as the
-category CPM %~\cite{cpm}
-or the language of superoperators, this model
-is purely algebraic, with a graph-like representation which does not involve exponentially-sized matrices. Finally, unlike
-existing semantics, we believe that it is extendable to express
-computations parametric on the size of the input (such as
-\emph{e.g.}~parametric families of circuits).
-}
-
-\REM{Is the following foundational ?
-Although not part of this proposal, the \azx approach could
-open the door to using quantum simulators for some general quantum
-computation  tasks.}
+The concept of a `deep' quantum compiler is entirely novel. Integrating optimisation and error correction intelligently into the stack gives a completely new set of tools for developing and using quantum computers.
+  Using the \zxcalculus to manage resources in quantum hardware is a totally new application of the \zxcalculus, and an ambitious new way to realise computations on heterogenous quantum hardware.
+%  Unlike sequences of gates, the tensor networks which are the terms of the \zxcalculus have no preordained causal structure beyond the global input and output, helping us to achieve optimal implementations on diverse architectures.
+Furthermore, our system allows transformations of tensor networks which cannot be expressed as equations between circuits as illustrated in the figure on the previous page.
+  In addition, the \zxcalculus is a sound and complete formal system for transforming quantum procedures, so that each program transformation which our compiler system comes with a proof of its correctness.
+  The way that the \zxcalculus represents quantum procedures also avoids the immediate dimensional explosion associated with explicit matrices, so that it will in many cases be more efficient than any other automated technique for reasoning about quantum procedures.
+The categorisation of multiple post-classical resources is also novel, as is the incorporation into the compiler chain. The development of a compiler stack that also doubles as a benchmarking tool is entirely new.
 
 
 \paragraph{Ambition:}
 \label{sec:ambition}
 
-  Our goal is to develop technology for a ``deep compiler'' for quantum computing systems: 
-  \begin{itemize}
-  \item
-    one which allows for the modular design of the quantum software stack, allowing programmers to write at a high level for any hardware and any quantum error correcting technology; but 
-  \item
-    such that the result is a tightly integrated piece of software upon compilation, and well-tailored to the specific resources, architecture, control systems, and hardware of a specific platform.
-  \end{itemize}
+  A ``deep compiler'' for quantum computing systems allows for modular design of the software stack. This lets programmers write at a high level for any hardware and any quantum error correcting codes. It is nevertheless tightly integrated upon compilation. In addition, it is fully tailored to the specific resources, architecture, control systems, and hardware of a specific platform. Furthermore the project includes isolating, integrating, and then certifying quantum speed-up.
   %\texttt{\bfseries \color{red!70!black}[refer to specific platforms here (NQIT + Grenoble)?]}
-  This is very technically ambitious: but while it has never been done before, we believe it to be achievable on the basis of our earlier work.
-
-\REM{
-Our central aim is to define, in \azx, (i)~a~formal tool to express formally verified code transformation and
-optimisation, (ii)~a~strictly more expressive superset of the existing semantics of programming languages, and (iii)~use this as an intermediate representation to provide a scalable solution for quantum software development, which is fully independent of the hardware. To our knowledge this is the first attempt of this kind: in view of the changing landscape of backends, defining a hardware-independent IR will be challenging.
-}
+  This is very technically ambitious: but while it has never been done before, we believe it to be achievable on the basis of our earlier work, and the ideal combination of skills within the project consortium.
 
-\BREM{(The following has been moved here from the description of \ref{task:NQIT-model} to put it more approximately where it can be of use) --- 
-For NQIT, the most important aspect is the fact that the modular
-architecture motivated using lattice surgery on surface codes for the
-logical operations, and that these are in effect be red/green copies
-and products. This will certainly make the ambition here much more
-achievable. 
-Annotations for dealing with byproduct operations in real-time or
-otherwise, particularly for magic states, is an early task to be dealt
-with. It is possible that work on \azx\ might inform the way in which
-NQIT networks its encoded memories together, if the problem of
-resource management can be fruitfully solved with particular layouts
-of logical qubits. 
-}
 
-\REM{More here}
 
 \paragraph{Foundational Character:}
 \label{sec:foundational-nature}
@@ -413,17 +342,15 @@ of logical qubits.
 All other systems take the gate model of quantum computing as a given.
 This is natural, as it is the \emph{lingua franca} of quantum computation researchers.
 The project proposes a new foundation for quantum software, based on a flexible  tensor-based representation, combined with mathematically rigorous semantics and formal verification.
-The deep quantum compilation technology which we develop
-will allow the computer to do the heavy lifting of managing resources and mapping operations onto the quantum hardware, allowing both the developers of hardware and software to focus their attentions elsewhere.
-This will facilitate the development of new architectures and technologies for quantum computing.
-A key example, exploited in our collaboration with NQIT, is that lattice surgery operations on surface codes do not fit into the gate model, but have natural and simple representations in the \zxcalculus \cite{BH-2017}.
+The ability to demonstrate quantum speed-up at compile-time will enhance our understanding of quantum information.
+The deep quantum compiler we will develop
+will do the heavy lifting of managing resources and mapping operations to quantum hardware, %allowing the developers of both hardware and software to focus elsewhere.
+%This will 
+facilitating the development of new architectures and technologies for quantum computing.
+A key example, exploited by NQIT and others, is that lattice surgery operations on surface codes do not fit into the gate model, but have simple representations in the \zxcalculus \cite{BH-2017}.
+
 
 
-\REM{
-While the \zxcalculus is
-restricted to qubits, the structures it uses are totally generic
-\cite{Duncan2016Interacting-Fro}, permitting \azx to handle qudits or codewords in a uniform manner.
-}
 
 \subsection{Concept and methodology}
 \label{sec:concept-methodology}  
@@ -443,12 +370,11 @@ multiple options and to address high scientific and technological
 risks.
 }
 
-Our proposed quantum compiler technology, which we call the \dzxc (``\emph{deep ZX compilation}'') system, is an advanced \textsc{zx}-style system
+The proposed \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. 
+$\lambda$-calculus in classical computing providing a solid but
+austere theoretical foundation. %, without any niceties for practical usage. 
 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.
@@ -463,9 +389,10 @@ completeness \cite{Jeandel2017A-Complete-Axio,HFW},
 and allowing us to leverage techniques from earlier work (cf.~\texttt{quantomatic}~\cite{Kissinger2015Quantomatic:-A-} and~\texttt{PyZX}~\cite{DKPdW-2019}). %, as well as new techniques developed as part of this project,
 This denotational kernel specifies the
 process to be carried out, independent of the target platform.  Many
-important transformations can be performed at this platform
-independent level --- without recourse to matrix representations of
-the operations involved --- such as simplifying the tensor network,
+important transformations can be performed at this %platform independent 
+level,
+%--- without recourse to matrix representations of the operations involved ---
+ such as simplifying the tensor network,
 reducing Clifford fragments to minimal forms, and reducing T-count.
 Development of such techniques is a low-risk extension of earlier
 work, and will be done early in the project
@@ -473,64 +400,52 @@ work, and will be done early in the project
 a program can be translated to a fault-tolerant equivalent with
 respect to a chosen error-correcting code.
 
-% \REM{Can do useful stuff at this level!  Some optimisation; ECC
-% simple generic optimisations.  e.g.
-%   \begin{itemize}
-%   \item reduce T-count / gate count
-%   \item coalesce Cliffords
-%   \item Circuits: minimise depth
-%   \item MBQC : minimise rounds
-%   \end{itemize}
-% }
-
-
-% specifying how the tensor
-% network may be realised.  This consists
-
-
 
 The annotations of the second layer provide the basis of \emph{augmented
-  rewrites}: program transformations which are guided by the
-annotations to achieve particular goals, not expressible in the basic
-tensor language.  For instance, there is an efficient algorithm
+  rewrites}: program transformations guided by the
+annotations to achieve particular goals. %, not expressible in the basic tensor language.  
+For instance, there is an efficient algorithm
 \cite{Mhalla:2008kx} to find the \emph{gflow} of a graph state; if the
 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}.
 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.
+ generalises this concept to include other annotation information to inform re-writing. 
+% 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, 
 the \dzxc system could incorporate
-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}).
-This would enable the \dzxc system
-to re-write procedures, minimising the number of operations, subject to the constraints described by those annotations.
-
-The \dzxc system will 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
-%to the trajectories of physical qubits, or subgraphs corresponding to
-%the primitive hardware operations and the time required to execute
-%them.  For
-%%hybrid architectures like NQIT, the annotations will also
-%%indicate the differing behaviour of the subsystems.
-Augmented
-rewrites will be used to find a runnable implementation of the
-abstract tensor for the target platform, and to optimise resource use.
+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-tolerance (\ref{task:ECC}).
+
+The \dzxc system will be modular, allowing for several different systems of annotations.
+The \dzxc system
+will re-write procedures, minimising the number of operations, subject to the constraints described by those annotations.
+  One such system of annotations will be to describe
+the constraints and the costs of operations for particular hardware (\ref{task:runnable}).
+%Augmented
+%rewrites will be used to find a runnable implementation of the
+%abstract tensor for the target platform, and to optimise resource use.
 The development
 of the general theory of annotations and augmented rewrites
 (\ref{task:annotate1}, \ref{task:annotate2}), algorithms for inferring
 specific annotations (\ref{wp:representation}), and rewrite strategies which exploit them
-(\ref{task:opt-machine}) form a major novel component of the project.%
-%
-%  (have I implemented
-% the correct process?) and  layer (is the implementation
-% possible/efficient/robust?).  This separation
-%
+(\ref{task:opt-machine}) form a major novel component of the project.
+
+%The \dzxc system
+%can therefore re-write procedures, minimising the number of operations, subject to the constraints described by those annotations.
 %
+%The \dzxc system will 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}).
+%Augmented
+%rewrites will be used to find a runnable implementation of the
+%abstract tensor for the target platform, and to optimise resource use.
+%The development
+%of the general theory of annotations and augmented rewrites
+%(\ref{task:annotate1}, \ref{task:annotate2}), algorithms for inferring
+%specific annotations (\ref{wp:representation}), and rewrite strategies which exploit them
+%(\ref{task:opt-machine}) form a major novel component of the project.%
 
 Concrete tensor networks have a fixed finite size, whereas algorithms
 are described in parametric fashion, \eg varying according the
@@ -539,12 +454,7 @@ To accommodate this, the \dzxc system would incorporate
 a second class of annotations to represent limited forms of iteration and recursion, yielding \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
 high-level quantum procedure provided as input.
-% --- The following commented out as I'm not sure what it means or if it contributes to the meaning of the proposal:
-% As this information is typically erased by the circuit generation phase
-% \cite{Alexander-S.-Green:2013fk,Cross2017Open-Quantum-As} of
-% compilation, we effectively move the boundary between \azx and the HLL
-% above the circuit-level.
-This is possibly the most challenging part
+This is a challenging part
 of the project (\ref{task:betterboxes}); however, we have experience of
 similar constructs from the \texttt{quantomatic}
 project~\cite{KZ:2015:aa, Kissinger2015Quantomatic:-A-}.
@@ -849,115 +759,115 @@ We will promote these cross-disciplinary interactions by a number of our planned
 \subsection{Expected impacts}
 \label{sec:expected-impacts}
 
-\newt{The \dzxc system} significantly advances the state-of-the-art across \newt{six of the seven} expected impacts.% the seventh is out of project scope.
+\REM{Be specific, and provide only information that applies to the proposal and its objectives. Wherever possible, use quantified indicators and targets.
+Describe how the project will contribute to the expected impacts (see ‘Research Targeted in the Call’ of the Call Announcement).
+Describe the importance of the technological outcome with regard to its transformational impact on technology and/or society.}
 
-\KILL{\texttt{\bfseries \color{red!70!black} [Some of these may need shortening a bit, particularly as we add material for the new Expected Impacts.]}}
+DZXC significantly advances the state-of-the-art across six of the seven expected impacts.
 
 \paragraph{Develop a deeper fundamental and practical
   understanding of systems and protocols for manipulating and
   exploiting quantum information ---\!\!}
+   
+  %The project will \textbf{develop a deeper fundamental and practical understanding} of systems for quantum information processing.
+  This project will take practical insights from different quantum technologies, along with fundamental techniques in quantum information processing, and embody them in the {\dzxc system}.
+We will develop a deep quantum compiler that can take input in several high-level quantum programming languages, automatically add error correction, optimise the process, and output machine instructions for different devices.
+Creating such a system necessarily will produce foundational insights into the capability of quantum devices, and quantum information as a physical phenomenon.
+The system can also interface with current models of quantum computing, and will enable new hybrid procedures to be developed, as well as potentially new forms of information processing via the \zxcalculus.
+Furthermore, expressing recursion will impact on our understanding of quantum causality.
+An exciting element of the project is isolating a set of demonstrably-quantum resources, and using these to confirm the presence of quantum speed-up. This will give significant insight into what is possibly `the' foundational question of quantum computing.
+The result of this project will be a step-change in our ability to describe how different quantum technologies store and manipulate information, and to design protocols that use their specific abilities.
 
-This project will take practical insights into the workings of diverse quantum technologies, along with fundamental techniques in quantum information processing, and embody them in the \newt{\dzxc system}. By embodying this expertise in \newt{a compiler system}, practitioners can employ push-button optimisations and fault-tolerant transformations of programs \newt{during compilation without needing} a deep understanding of the underlying theoretical techniques, effectively making these techniques available to a broader audience.
 
-The \newt{\dzxc system will compile from high-level (algorithmic) to low-level (physical) representations, allowing programmers to write at a high level for any hardware and any quantum error correcting technology.}
-For instance, causal and topological structure is a crucial restriction on what can be processed in networked computing, \newt{the \dzxc system will be able to take this into account when compiling.}
-The project also includes the ability to interface with current models of quantum computing (the circuit and one-way models), and will enable new hybrid procedures to be developed that include elements of both (as well as potentially new forms of information processing represented in \newt{the annotated \zxcalculus}).
-The result of this project will be a step-change in our ability to describe how different quantum technologies store and manipulate quantum information, and to design protocols that use their specific abilities.
+
+% By embodying this expertise in \newt{a compiler system}, practitioners can employ push-button optimisations and fault-tolerant transformations of programs \newt{during compilation without needing} a deep understanding of the underlying theoretical techniques, effectively making these techniques available to a broader audience.
+%
+%The \newt{\dzxc system will compile from high-level (algorithmic) to low-level (physical) representations, allowing programmers to write at a high level for any hardware and any quantum error correcting technology.}
+%For instance, causal and topological structure is a crucial restriction on what can be processed in networked computing, \newt{the \dzxc system will be able to take this into account when compiling.}
+%The project also includes the ability to interface with current models of quantum computing (the circuit and one-way models), and will enable new hybrid procedures to be developed that include elements of both (as well as potentially new forms of information processing represented in \newt{the annotated \zxcalculus}).
+%The result of this project will be a step-change in our ability to describe how different quantum technologies store and manipulate quantum information, and to design protocols that use their specific abilities.
 
 
 \paragraph{Enhance the robustness and scalability of quantum
   information technologies in the presence of environmental
   decoherence ---\!\!}
   
-\newt{The deep compilation provided by the \dzxc system} will help minimise the resource requirements in quantum technologies, \newt{as well as adapting to the individual requirements of} different hardware platforms.
-\newt{The \dzxc system will be able to} model environmental noise and error rates of the target platform, allowing the compiler to make provisions to minimise decoherence as the program runs.
-In particular, the annotation layer of \newt{the \zxcalculus} can be used for
-fine-grained resource management for lower levels of error correction as well as idealised quantum memories, allowing integration of compilation and protection of coherence.
-\newt{The \dzxc system} will enhance the development of error correction that is tailored to specific devices.
-Individual noise models and error propagation will be encoded in the \newt{\zxcalculus} through annotations, which can then be used for optimisation of error correction procedures.
-Using \newt{the annotated \zxcalculus} as a design tool, specific error correction protocols can be developed for different devices, customised to the different noise models.
+The deep compilation techniques provided by the \dzxc system will reduce the resource requirements in quantum technologies via built-in optimisation techniques.
+The latter will be based in part on our already state-of-the-art research (cf.\ \S~\ref{sec:basel-knowl-skills}).
+
+We will develop new layers of annotations for the \zxcalculus and use them for fine-grained resource management around noise, error rates, and connectivity.
+Using the annotated \zxcalculus as a design tool, specific error correction protocols can then be developed for different devices, customised to the different noise and error propagation models.
 These models will be flexible as the devices get larger, ensuring scalability of robust devices.
-Networked scalability can be optimised for, as well as different topologies, by encoding timing and spacial constraints in the language.
-\newt{With the annotated \zxcalculus as} a common representation, hybrid devices can also be optimised for. Error correction or mitigation strategies can be developed across multiple devices acting in tandem.
-Modelling error correction in \newt{the annotated \zxcalculus} will thus enable the design of new error correction procedures, optimisation of existing ones, and give a mutually-intelligible language for error correction theorists and device technologists, \newt{all integrated in the \dzxc system}.
+Processes can be optimised for networked scalability and diffferent topologies by encoding timing and spacial constraints in the language.
+With the annotated \zxcalculus as a common representation, hybrid devices can also be optimised for.
+Error correction or mitigation strategies can be developed across multiple devices acting in tandem.
+
+Since the \dzxc system is based on the \zxcalculus as an intermediate representation, this allows the integration of compilation and protection of coherence.
+It also enables the system to adapt and optimise protocols for the individual requirements of different hardware platforms.
+% and give a mutually-intelligible language for error correction theorists and device technologists, all integrated in the \dzxc system.
 
 
 \paragraph{Identify new opportunities and applications fostered
   through quantum technologies, and the possible ways to transfer
   these technologies from laboratories to industries ---\!\!}
 
-%doing cool stuff with cool stuff
+As the basis of a retargetable compiler, the \dzxc system will make it easy to support new quantum devices.
+This will help make the latest developments in quantum technology available to all academic and industrial users, maximising the return on investment in quantum computing.
+To help non-specialist users, we will provide the ability to apply complicated transformations -- such as the introduction of error correction or the optimisation of sequences of operations -- fully automatically or at the push of a button.
 
-\newt{The purpose of the \dzxc system is to form the basis of a retargetable compiler, making it easy to support new quantum devices.
-This will help to make the latest developments in quantum technology available to all academic and industrial users,  maximising the return on investment in quantum computing.}
-Our consortium includes an industrial partner (\newt{Cambridge Quantum Computing}) to help ensure the industrial relevance of our work.
-We also have \newt{experimentalists} on the advisory panel.
-With \newt{the \dzxc system}, high-level quantum languages and protocols can be designed without needing to know the underlying hardware.
+Our consortium includes an industrial partner, Cambridge Quantum Computing, to help ensure the industrial relevance of our work.
+We will also work closely with quantum technologies groups at QuEnG and NQIT to check the applicability of our work.
+
+With the \dzxc system, high-level quantum languages and protocols can be designed without needing to know the underlying hardware they will eventually be run on.
 This will streamline the production of quantum software, opening it up to individuals and companies with limited prior knowledge of quantum computing. 
-Quantum hardware will also be more accessible, both in academia and industry. Individual developers will not need to know the entire architecture, as different elements can be \newt{adapted to automatically during compilation}.
+Quantum hardware will also be more accessible, both in academia and industry.
+Individual developers will not need to know the entire architecture, as different elements can be adapted automatically during compilation.
 This will accelerate the widespread commercial and academic development and exploitation of quantum technology.  
 
 
-% and programming languages
-% will become more easily transferred 
-
-% accelerating the widespread exploitation of
-% quantum technology.  
-
-% to different hardware platforms,
-
-
-
-% and accessible to both academia and industry.  
-
 \paragraph{Enhance interdisciplinarity in crossing traditional
   boundaries between disciplines in order to enlarge the community
   involved in tackling these new challenges ---\!\!}
 
-%The inherently interdisciplinary nature of this project will bring a larger community to bear solving problems during the lifetime of the project. The development of the \azx language and compiler stacks themselves will also open up further challenges as the project progresses (and beyond) that are accessible to broader communities. 
-\newt{The \dzxc system} will connect the entire range of knowledge involved in building quantum technologies, from experimental and theoretical Physics, through to quantum computing theory, and on to formal methods of Computer Science.
-All of these are needed to develop the deep compilation system, \newt{so developing the \dzxc system} is a fundamentally interdisciplinary task.
-\newt{By aiding the development of intuitively accessible programming languages, the \dzxc system will also make quantum technologies accessible to a broader range of users and developers. 
+Developing the \dzxc system will utilise the entire range of knowledge required for building quantum technologies, from experimental and theoretical physics, through to quantum computing theory and foundations, and on to formal methods of computer science.
+All of these are needed to develop the deep compilation system, so developing the \dzxc system is a fundamentally interdisciplinary task.
+Via its intelligent compilation chain and by aiding the development of intuitively accessible programming languages, the \dzxc system will also make quantum technologies accessible to a broader range of users and developers.
 For example, algorithm and protocol designers will not need to interface directly with quantum technologies in order to test the effectiveness of their work, lowering the bar for development in the field.
-End-users outside of quantum physics and computer science will also be able to build protocols for use in their own field that do not require them to understand the physical action of the hardware.}
+End-users outside of quantum physics and computer science will also be able to build protocols for use in their own field that do not require them to understand the physical action of the hardware.
 
 The \dzxc system will not be a closed system: our commitment to open
-APIs (See \ref{task:trans1} and \ref{task:backendapi}) and our open
-test suite (~\ref{task:testBench}) will enable users from outside the
-project to integrate new tools and techniques with \dzxc and engage
+APIs (see \ref{task:trans1} and \ref{task:backendapi}) and our open
+test suite (\ref{task:testBench}) will enable users from outside the
+project to integrate new tools and techniques with the \dzxc system, and engage
 the wider community.
 
-The advent of quantum computation, and the diverse set of skills needed to bring an idea from algorithm to implementation, has shown the limitations of traditional subject boundaries. The breadth of expertise of this consortium, and its thematic focus on developing a common language and methodology from quantum technologies will help overcome these limitations within the project and in the wider community.
+The advent of quantum computation, and the diverse set of skills needed to bring an idea from algorithm to implementation, has shown the limitations of traditional subject boundaries. The breadth of expertise of this consortium, and its thematic focus on developing a common language and methodology from quantum technologies will help transcend these limitations within the project and in the wider community.
 
 
 \paragraph{Spread excellence throughout Europe by involving partners from the widening countries ---\!\!}
-\newt{The ICTQT is a newly founded research institute in the strongly emergent Poland. The university of Gdansk, host of the institute, has a long prominent track record on quantum information theory, with the core of entanglement theory itself having been developed there. Sainz's newly founded Foundational Underpinnings of Quantum Technologies group, strives at contributing to and complementing the existing team in Gdansk, by bringing in the new scope of process theories to tackle foundational and applied questions about quantum theory. Her own team, funded by ICTQT, will initially consists of a postdoctoral research fellow and a PhD student (both TBA). 
+One of our consortium partners is based at the ICTQT, a newly founded research institute in the strongly emergent Poland.
+The university of Gdansk, host of the institute, has a long prominent track record on quantum information, with the core of entanglement theory having been developed there.
+Sainz's newly founded Foundational Underpinnings of Quantum Technologies group will contribute to and complement the existing team in Gdansk by bringing in the new scope of process theories to tackle foundational and applied questions in quantum theory.
+Her own team, funded by ICTQT, will initially consist of a postdoctoral research fellow and a PhD student.% (both TBA).
+Oxford site head Coecke was involved in establishing Sainz's new team at Gdansk's new ICTQT institute, as a member of the institutes' International Scientific Committee. The scope of this research proposal aligns perfectly with part of the mission statement of Sainz's team, namely the study of process theories.
+
+%\TODOb{Is this paragraph in the right section? Some of it seems more ``first-time participants''-ey}
+%Oxford site head Coecke was involved in establishing Sainz's new team at Gdansk's new ICTQT institute, as a member of the institutes' International Scientific Committee.
+%With this project we involve this new institute, and Sainz's team in particular, within an established research community for mutual exchange of knowledge.
+%The scope of this research proposal aligns perfectly with part of the mission statement of Sainz's team, namely the study of process theories.
+%As the ``Swiss army knife'' of process theories, the \zxcalculus will bring the foundations of quantum theory in direct contact with quantum technology.
+%More generally, the experienced project partners will adopt a mentoring role towards this newly formed ICTQT group.
 
-Oxford site head Coecke was involved in establishing Sainz's new team at Gdansk's new ICTQT institute, as a member of the institutes' International Scientific Committee. With this project we involve this new institute, and Sainz's team in particular, within an established research community. The particular scope of this research proposal perfectly aligns with part of the mission statement of Sainz's team, which comprises the study of process theories, since ZX-calculus is the ``Swiss army knife" of process theories, bringing them in direct contact with quantum technology. More generally, the experienced project partners will adopt a mentoring role towards this newly formed ICTQT group.
-}
-%\newt{The ICTQT is a newly founded research institute in the strongly emergent Poland. The university of Gdansk, host of the institute, has a long prominent track record on quantum information theory, with the core of entanglement theory itself having been developed there. Sainz's newly founded Foundational Underpinnings of Quantum Technologies group, strives at contributing to and complementing the existing team in Gdansk, by bringing in the new scope of process theories to tackle foundational and applied questions about quantum theory. Oxford site head Coecke was involved in establishing Sainz's new team at Gdansk's new ICTQT institute, as a member of the institutes' International Scientific Committee. With this project we involve this new institute, and Sainz's team in particular, within an established research community. The particular scope of this research proposal perfectly aligns with part of the mission statement of Sainz's team, which comprises the study of process theories, since ZX-calculus is the Swiss army knife of process theories, bringing process theory in direct contact with quantum technology. More generally, the experienced project partners will adopt a mentoring role towards this newly formed ICTQT group.} 
 
 \paragraph{Build leading innovation capacity across Europe by involvement of key actors that can make a difference in the future, for example excellent young researchers, ambitious high-tech SMEs or first-time participants ---\!\!}
-\newt{The consortium team is well-balanced between young and
-  established researchers. We are building innovation capacity by
-  involving many excellent early-career researchers as well as several
-  research groups that have been founded in the past few years, namely
-  those of Horsman, Kissinger, Valiron, and Sainz (the latter shortly
-  to be established at the proposal writing phase; see previous
-  paragraph). The team also includes senior researchers on the brink
-  of %of
-   group development (Backens, de Beaudrap, Wang). With team
-  members like Coecke who had over 30 grants including several large
-  networks, know-how on project design at the drafting stage to
-  execution will carry over to the more junior partners, as Coecke
-  will adopt a mentoring role throughout the project. Our industrial
-  partner, CQC, is an ambitious high-tech SME, who are currently leading
-the sector in high performance compilation of quantum software.  The
-CQC team leader, Duncan, is an experienced researcher who brings
-expertise in technology transfer from academia to industry.  The
-junior team members at CQC will benefit from exposure to the latest
-research, while the younger academics will benefit from interaction
-with industry.} 
+The consortium team is well-balanced between young and established researchers.
+We are building innovation capacity by involving several research groups that have been founded in the past few years, namely those of Horsman, Kissinger, Valiron, and Sainz (the latter shortly to be established at the proposal writing phase; see previous paragraph).
+The team also includes other excellent young researchers on the brink of group development (Backens, de Beaudrap, Wang).
+With team members like Coecke who had over 30 grants including several large networks, know-how on project design at the drafting stage to execution will carry over to the more junior partners, as Coecke will adopt a mentoring role throughout the project.
+Our industrial partner, CQC, is an ambitious high-tech SME.
+Indeed, CQC is currently leading the sector in high performance compilation of quantum software.
+The CQC team leader, Duncan, is an experienced researcher who brings expertise in technology transfer from academia to industry.
+The junior team members at CQC will benefit from exposure to the latest research, while the younger academics will benefit from interaction with industry.
 
 
 \subsection{Dissemination, exploitation of results, communication}