<html><head><meta name="color-scheme" content="light dark"></head><body><pre style="word-wrap: break-word; white-space: pre-wrap;">% !TEX TS-program = pdflatexmk 
\RequirePackage[l2tabu,orthodox]{nag}
\documentclass[11pt,a4paper]{article} 
\usepackage{etex}



%%%% do rwd stuff %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\pdfoutput=1
%\usepackage{rwd-drafting}
\usepackage[suppress]{rwd-drafting} 
\input{margins.tex} % font and other formatting in here
\input{preamble.tex}


\usepackage{wrapfig}
\usepackage{diagrams}  
\input{figures/cnot.tex}  

\begin{document} 

\newcommand\projtitle{Deep quantum compilation using the ZX-calculus}
\newcommand\projacro{DZXC}  

\title{QuantERA Full Proposal}    
\author{}
\date{} 
\maketitle 

\begin{center}
  {\Huge \projacro :}\\[1ex] 
  {\LARGE \projtitle } 
\end{center}

\newpage
%\textit{Title page will be replaced with file Front-Page\\
%\oldt{Text from previous proposal in blue}}
%\newt{/ Very recent revisions for the new proposal are in violet}
  
\REM{\textbf{Everything below this needs to fit under 4000 
    characters for the online submission system}}

\paragraph{Duration:}  36 months
\label{sec:duration}



\section*{Summary of the project \REM{Same as long proposal}}

\label{sec:abstract}
%currently 2510 characters

  \REM{(publishable abstract, max. 1/2 page): Be precise and
    concise. This summary will be used to select suited reviewers for  
    the proposal.}  

We propose the development of ``deep quantum compilation" technology. This is the concept of a compiler for quantum systems which can be used to develop large portions of the software stack, in a way which is modular in design but tightly integrated once compiled. We propose to develop deep quantum compilation technology by leveraging the \zxcalculus, a versatile formal tool to efficiently reason about tensors, which recently demonstrated state-of-the-art capability to optimise unitary circuits. The graphical \zxcalculus has recently also be shown to be complete: all equations that hold in standard quantum theory can be derived in \zxcalculus. This provides us with the opportunity to develop compiler technology with a scope that would be difficult to achieve otherwise. 

Recent investment in quantum technologies has brought us into the era of noisy intermediate-scale quantum (NISQ) devices. These computers are patchworks of components (including classical) that vary greatly between implementations such as silicon qubits, superconducting circuits, or ion traps. As the technology matures into the fault-tolerant regime, quantum computers will continue to be accompanied by a myriad of control systems, and a scarcity of resources. Programming such devices currently requires intimate knowledge of the hardware, and programs must be rewritten for every new device to closely match the hardware model. Any optimisation is purely ad-hoc. We face a situation where the ever-multiplying range of quantum computers has minimal software support. 

Solving this problem requires a ``deep" quantum compiler -- one which can transform algorithms to match the resources and capabilities of diverse hardware platforms. Recent formal and practical advances in completeness and optimisation of the \zxcalculus demonstrate a proof-of-principle of the possibility of developing a deep quantum compiler, including provably-correct program transformations for automatically adding error correction and performing hardware-guided optimisations. We will target the compilation stack for three of the most promising hardware platforms, and develop the techniques and software tools to build a deep compiler. In addition, leveraging the foundational expressiveness of the calculus, we will isolate specific resources that give rise to quantum processing, providing in-compiler certification of quantum speed-up. Developing a ``deep" compiler will allow for the sound development of tightly integrated software stacks for quantum computers, becoming a standard for optimisation and benchmarking, and enabling quantum devices to perform computations demonstrably better and faster. 
 
%The goal of this project is to develop the flexible intermediate  for compilation and optimisation, which is necessary for the immediate-term practical implementation of post-classical protocols on noisy intermediate-scale quantum computers. %how many buzzwords can we get in this sentence


\section*{Relevance to the topic addressed in the call \REM{Same as long proposal}}
\label{sec:relev-topic-addr}
%currently 1274 characters

\REM{(in particular specify here which part of the call text is
  concerned by your project, max. 1/4 page):}
  
  The project clearly comprises ``\textit{transformative research}'' that explores ``\textit{collaborative advanced interdisciplinary science and/or cutting-edge engineering with the potential to initiate or foster new lines of quantum technologies}'', which is the key overall objective of QuantERA. 
We include several ``\textit{excellent young researchers}'', including from Poland, and partner with Cambridge Quantum Computing, a clearly ``\textit{ambitious high-tech SME}''. 
 In particular we address the \textit{Quantum Computation} area of the call. 
 The
retargettable nature of the compiler supports ``\emph{new architectures
  for quantum computation}", in particular technologically heterogeneous
implementations.  The optimising aspect of the compiler will allow the
``\emph{optimisation of error correction codes}", at both
intermediate and machine level.  The ability to compile multiple
high-level languages will promote the ``\emph{development of novel
  quantum algorithms}". Machine-dependent optimisation work will contribute to the ``\textit{development of devices to realise multiqubit algorithms}".
  The ability to compile with specifically post-classical resources leads directly to ``\textit{demonstration of quantum speed-up}". 
  In total, this project is an enabling
technology that multiplies the impact of all the target 
outcomes of QuantERA and the Quantum
Technology Flagship.
  
  \REM{ FROM CALL DOCUMENT:
  The QuantERA consortium has created a common funding instrument to support European research projects enabling long-term research in the area of Quantum Technologies.
Through this instrument, the national/regional funding organisations of the QuantERA consortium contribute to the Quantum Flagship agenda1. By launching joint European calls for research projects, they can support more diverse research communities, who are able to tackle the most challenging and novel research directions.
 QuantERA projects should be of a FET-like nature and contribute to the development of the European research and innovation in Quantum Technologies. The transformative research done in QuantERA should explore collaborative advanced interdisciplinary science and/or cutting-edge engineering with the potential to initiate or foster new lines of quantum technologies and help Europe grasp leadership early on in promising future technology areas.
 **warning this paragraph is patronising bullshit, fuck this "spreading research excellence" western-euro superiority nonsense:
 To spread research excellence throughout Europe, QuantERA projects are encouraged to include partners from the widening countries participating in the call: Bulgaria, Croatia, Czech Republic, Hungary, Latvia, Lithuania, Poland, Portugal, Romania, Slovakia, Slovenia and Turkey.
 
To build leading innovation capacity across Europe and connect with industry, QuantERA projects are encouraged to involve key actors that can make a difference in the future, for example excellent young researchers, ambitious high-tech SMEs etc.
3. Quantum computation
Development of devices to realise multiqubit algorithms; demonstration and optimisation of error correction codes; interfaces between quantum computers and communication systems.
Development of novel quantum algorithms; demonstration of quantum speed-up; new architectures for quantum computation.
}


\newpage
\section{EXCELLENCE \REM{(6 pages, same as long proposal)}}
\label{sec:overview}

\subsection{Targeted breakthrough, baseline of knowledge and skills}
\label{sec:targ-breakthr-basel}

\REM{
Describe the targeted breakthroughs of the project. 
Describe how the science and technology contribute to the establishment of a solid baseline of knowledge and skills for the specific theme addressed. 
Describe the specific objectives of the project, which should be clear, measurable, realistic and achievable within the duration of the project.
}

\paragraph{Summary: } 
\label{sec:summary:-}

  We propose to develop \emph{deep quantum compilation technology}.
  This consists of techniques for a compiler to translate high-level specifications of quantum programs to operations on a variety of hardware platforms, automatically managing resources and architectural constraints in doing so. It uses the \zxcalculus, already the lead tool in circuit optimisation.  This allows the software stack to be developed and organised in a modular fashion for multiple platforms, and then compiled in an intelligently-managed way. The addition of compile-time certification of quantum speed-up completes the ability of the deep compiler to make the most of valuable quantum hardware resources.

%\TODOb{Summary/context should contain a clear statement that NOW zx does better (i.e. "outperforms") than anything else for circuit simplification using PyZX.  This should be explained in even more detail elsewhere.  Aleks maybe?}

\paragraph{Context:}
\label{sec:context}  
  Effective programming practice allows the programmer to design software without paying very close attention to the nature of the hardware.
  In the context of quantum technologies, this is made difficult by the fact that  hardware platforms are varied~\cite{PhysRevX.4.041041,Raussendorf-2001,KendonAncilla}\REM{[double-check this list of references for suitability]}, have limited resources, and are evolving quickly.
%  Due to the overhead involved in making quantum computations fault-tolerant, different platforms will continue to be developed for different tasks (with and without error correction), even as quantum hardware technologies mature and demonstrate scalability.
%  The complications presented by limited resources and divergent architectures will likely persist for the foreseeable future.
  For classical programs, modern compiler toolchains such as LLVM (\url{llvm.org})
  %\footnote{% The LLVM Compiler Infrastructure, \url{http://llvm.org}}
  decouple high-level programming from different hardware platforms, allowing for easy and customisable cross-compilation; no such tools exist for quantum devices.
  Optimisation, in particular around error correction overheads, will be vital for running post-classical protocols on near-term hardware. Classically, this is an element of an integrated compiler.
  As quantum technologies will continue to be scarce and valuable, identifying truly quantum resources, currently limited to magic states, will be a vital tool for optimising resource use, demonstrating speed-up, and benchmarking quantum devices and protocols.
  
To build the deep compiler combining all these elements we will use the \newt{graphical} \zxcalculus~\cite{BH-2017,HFW,JPV-2018,DKPdW-2019}. %the opportunity exists to develop a more ambitious version of the LLVM concept for quantum computing.
  %, bringing forward the day that quantum computers can be exploited for practical application.  
   This already outperforms all other formal methods for certain problems. For example, the {\tt PyZX} tool for quantum circuit optimisation is already obtaining state of the art results in T-count minimisation (cf.~theory in \cite{DKPdW-2019}), an important problem for effective fault-tolerant quantum computation.  This is a further development on the recently achieved ultimate milestone for graphical reasoning: all equations that hold in standard quantum theory can be derived in \zxcalculus (a.k.a.~`completeness') \cite{Jeandel2017A-Complete-Axio, HFW}.
 A deep-\zx compiler will significantly advance the deployment of practical quantum computing.
  

\paragraph{Targeted breakthrough:} 
\label{sec:targ-breakthr}

We will develop \emph{the \dzxc system} for deep quantum compilation.
    \begin{wrapfigure}{r}{0.50\textwidth}
    \vspace*{-10mm}%
%    \texttt{\color{red!70!black} [Placeholder?]} \\[-5ex]
    \hspace*{-4mm}%
    \cgraph[0.7]{dzxc-arch-diagram3.pdf}%
    \vspace*{-9mm}  
    \end{wrapfigure}
This set of tools will intelligently translate high-
level quantum programs to low-level operations on quantum hardware platforms, including
  \begin{itemize}
  \item
    incorporating architectural constraints
  \item
    optimising resource use
      \item
    certifying speed-up
  \item
     managing error correction.    
  \end{itemize}
These will be specified in a modular way but tightly integrated upon compilation.
  To demonstrate this technology, we will develop a \zxcalculus based compiler from a high-level quantum programming language to hardware, for (i)~coupled ion traps (NQIT)~\cite{PhysRevX.4.041041}, (ii)~silicon spin qubits (Grenoble)\REM{ [do we have something here to cite?]}, (iii)~an IBM device. %The compiler stack will include open APIs, and t
  The final milestone is a ready-to-run deep-zx compiler chain incorporating physical layout, error correction support and algorithmic optimisation, compiled for a target system, and demonstrating explicit post-classical resource use in a quantum computation.
  

%  We will specifically pursue the development of deep quantum compilation technology by exploiting the versatility of the \zxcalculus, and further developing its application. 
%This will greatly improve the software ecosystem for quantum computers:
%deep quantum compilation will allow future quantum devices to
%easily run existing programs, and future programming languages automatically gain support on a wide range of hardware.

\paragraph{Baseline of knowledge and skills:}
\label{sec:basel-knowl-skills}

  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.

  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.
  An analogue of LLVM for quantum systems would have to manage resources in spite of fundamentally quantum obstacles, such as the no-cloning theorem; and to be useful in the near term, it would also have to account for noise and the resources required for error correction, in addition to the functionality of the sort provided by LLVM.

  One way to realise a comparable compiler technology for quantum computers is to use the \zxcalculus~\cite{Coecke:2009aa}, which is a formal system for transforming quantum procedures in a way that preserves meaning.
  The \zxcalculus is the product of a decade of work by members of this consortium
   on the mathematical foundations of quantum computing \cite{AbrCoe:CatSemQuant:2004,
%Coecke:2009db, CDKW-lics:2012qy, 
  Coecke2017Picturing-Quant}, and can be viewed in two distinct ways: either (i)~as a formal axiomatic theory which encodes the properties of complementary observables in categorical algebra, or (ii)~as a symbolic notation for tensor networks representing quantum states and linear operators.
  Terms in the \zxcalculus are labelled graphs; equations in the calculus are reified as a small number of graph rewrite rules.
  This equational theory is frequently more tractable than working explicitly with matrix representations.  
  Recently, members of our consortium developed versions of the \zxcalculus which were complete for Clifford+T computations~\cite{Jeandel2017A-Complete-Axio,NW-2018} and for  quantum computations including CNOTs and arbitrary single-qubit gates~\cite{HFW,JPV-2018}.
  This means that one can formally prove every equality of quantum circuits in these gate models through the application of a small number of relatively simple rules for rewriting tensors.
This stunning achievement opens the door to many
new possibilities for optimisation and verification of quantum
computations. 

%  and is complete for important subtheories such as the stablizer
% fragment \cite{1367-2630-16-9-093021} and single qubit Clifford+T 
% equations \cite{Backens:2014aa}. 

%\REM{The closely related ZW-calculus \cite{Hadzihasanovic2015A-Diagrammatic-} provides a complete characterisation of qubit entanglement-classes.}

  The \zxcalculus %has been extensively applied to quantum computation, and
  is powerful and flexible, can easily describe computations in both the circuit and measurement-based models of quantum computation (MBQC)~\cite{Raussendorf-2001} and can be used to formulate and verify quantum error correcting codes \cite{Chancellor2016Coherent-Parity, Duncan:2013lr} and quantum algorithms \cite{Stefano-Gogioso2017Fully-graphical, Zeng2015The-Abstract-St}.  Its graphical representation is well-suited to describing systems which naturally have a graph structure, such as surface codes for topological cluster-states \cite{Horsman:2011lr}, and MBQC \cite{Duncan:2012uq}, where it has been used to translate \cite{Duncan:2010aa} between the 1-way model and the circuit model. \textit{\bfseries\ttfamily\color{red!70!black} \KILL{[Not sure whether we want to keep this paragraph but it has lots of good references]}}
  
\newt{The tensor network structure means that the \zxcalculus represents initial states, unitary operations, measurements and discarding in one unified notation.
It also makes the notation vastly more flexible than quantum circuits: \zx-based transformations between quantum circuits may have intermediate steps that cannot directly be expressed as equations between circuits \cite{DKPdW-2019}.
An example of such a transformation is the following:}

\includegraphics[width=\textwidth]{figures/circuit-fig}

Members of our consortium have demonstrated how to use these formal
reasoning techniques in software, including the interactive theorem
prover {\tt quantomatic} \cite{Kissinger2015Quantomatic:-A-} (which
was used to formally verify quantum communication protocols and error
correcting codes \cite{Chancellor2016Coherent-Parity,Duncan:2013lr})
and {\tt PyZX}~\cite{DKPdW-2019}, which provides an early
demonstration of the capacity of the \zxcalculus to \newt{outperform
  other methods of circuit optimisation,  in the sense that certain
  circuit metric (such as total size, tree-width, or number of
  non-Clifford subterms such as T-gates) can be minimised.}  Our
industry partner CQC develops \tket, a retargetable quantum compiler
which, using \zx-based optimisations, outperforms all existing
compilers for quantum software.
\TODO{citations if there is space, otherwise maybe kill the second half of this sentence.}
%%% cutting because repeated later
% It is strictly more powerful than the stabiliser
% formalism~\cite{Backens:2012fk}, 


%\begin{figure}[t]
%  \vspace{-2mm}
%  \centering
%  \[
%    \cnoti[0.7] \rTo^* 
%    \cnotii[0.6] \rTo^*
%    \cnotiii[0.6] \rTo^*  
%    \cnotiv[0.6] \rTo^* 
%    %\cnotv[0.6] \rTo^* 
%    \cnotvi[0.7]
%  \]
%  \vspace{-2mm}
%  \caption{The \zxcalculus in action:  translating from MBQC (left) to
%  a quantum circuit (right)}
%\label{fig:zx-mbqc-cnot}
%\end{figure}


\paragraph{Contribution to the theme addressed}
\label{sec:contr-theme-addr}

We specifically address the theme of \emph{Quantum Computation}.
  Our goal is to 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.

\subsection{Novelty, level of ambition and foundational character}
\label{sec:novelty-level-ambit}

\REM{Describe the advance your proposal would provide beyond the
  state-of-the-art, and to what extent the proposed work is ambitious,
  novel and of a foundational nature. \textbf{Your answer could refer
    to the ground-breaking nature of the objectives, concepts
    involved, issues and problems to be addressed, and approaches and
    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.}


\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}
  %\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.
}

\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}

\REM{More here. 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.}

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}.


\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}  

\REM{
Describe and explain the overall concept and research approach
underpinning the project. Describe the main ideas, models or
assumptions involved. Identify any interdisciplinary considerations
and, where relevant, use of stakeholder knowledge. 
\textbf{Describe any national or international research and innovation
  activities which will be linked with the project, especially where
  the outputs from these will feed into the project.}

Describe the methodology and explain its relevance to the objectives.
Describe the appropriateness of the methodology to narrow down
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
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. 
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.
This two-level design separates the specification (graph layer) from
the implementation (annotation layer) of the program, and is the key
to achieving our goal of supporting multiple targets.

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,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,
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
(\ref{task:algorithms},\ref{task:basic-opt}). Further, at this stage
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
\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.
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.
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
%
%

Concrete tensor networks have a fixed finite size, whereas algorithms
are described in parametric fashion, \eg varying according the
input size.
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
of the project (\ref{task:betterboxes}); however, we have experience of
similar constructs from the \texttt{quantomatic}
project~\cite{KZ:2015:aa, Kissinger2015Quantomatic:-A-}.
\REM{[apropos to refer to PyZX here?]}

We will develop translations for the \dzxc system from existing quantum programming languages~(\ref{task:trans1}) early in the project.
These will provide
 examples and test cases, and allow comparative
evaluation.

\BREM{
\begin{itemize}
  % \item methodology centres around common language: AZX
  % \item (\textbf{idea:} what about IZX, \textit{implemented} ZX?
  %   i.e. something more active/evocative than \textit{annotations})
  % \item this has two layers (1) the ZX-graph layer, a  technique for representing quantum processes, and (2) annotations which describe parameters as well as how process is implemented within a computational model
  % \item (1) already done (cf. ten years of research!)
  % \item (2) is guided in two ways: \textit{top-down} (capturing language features of Quipper) and \textit{bottom-up} (capturing hardware requirements)
  \item a common language synchronises the project across sites, implementation details (e.g. platform, language, etc.), and goals (optimisation, EC, simulation)
  \item development focuses around simple, modular tools, mitigating \textbf{risk} and increasing \textbf{agility} of the project as a whole
  \item 
\end{itemize}
}

\REM{
The front-end is responsible for translating a high-level programming
language to the IR.  We will adapt the existing \emph{Quipper}
compiler \cite{Alexander-S.-Green:2013fk} for this purpose. % We will
% develop static analysis techniques like abstract interpretation
% \cite{Perdrix2008} or implicit computational complexity
% \cite{DALLAGO2010377} to optimise various resources.  Such
% optimisations may be performed at the high-level or passed to the IR
% as annotations.
The front-end will later be adapted to generate the
parametric IR (see \ref{task:betterboxes}.)
}

\REM{These modules will be used to implement sophisticated
quantum algorithms which will serve as robust benchmarks
for the other WPs.   
idea of separating program compile time from circuit compile time
(following the {\em Quipper} and {\liquid} architecture).

  other objectives. Some program parameters and control flow features
  of the programming language will be translated into the \azx\
  representation.
}

The four major work packages of the project are structured into
various themes: the relation between \zx and other quantum computing representations (\ref{wp:frontend});  necessary theoretical developments of \zx (\ref{wp:representation}); optimisation strategies independent of implementations (\ref{wp:theory}); using annotated \zx to compile and optimise for specific quantum devices.(\ref{wp:usefulstuff}).

\subsubsection{A quantum compiler stack}
\label{sec:progr-lang-supp}

  Several powerful high-level languages (HLLs) have been proposed for
  quantum programs, such as Quipper~\cite{Alexander-S.-Green:2013fk},
  \Qsharp~\cite{qsharp}, and the Python framework
  ProjectQ~\cite{Steiger2016ProjectQ:-An-Op}.
  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.
  Our proposed \dzxc system will represent an interface between multiple different HLLs for quantum procedures, and various quantum hardware platforms.
  This system will use terms of the \zxcalculus as an internal representation of the procedure as it undergoes optimisations and translations, \newt{both abstractly and} 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.

  As most existing quantum HLLs can output circuit descriptions, and
  as circuits can easily be represented in the \zxcalculus, for the
  front-end of~\ref{task:HHL} will first focus on the circuit language
  QASM~\cite{Cross2017Open-Quantum-As} before moving towards the more
  expressive HHLs Quipper~\cite{Alexander-S.-Green:2013fk},
  \Qsharp~\cite{qsharp}, and
  ProjectQ~\cite{Steiger2016ProjectQ:-An-Op}. With this expertise we
  will then develop in Task~\ref{task:trans1} a general procedure
  allowing virtually any extant quantum HLL to interface with the
  \dzxc system.

%
  Moving down the compilation toolchain towards quantum devices
  requires the translation of \zx terms down to some lower-level
  representation, specific to each quantum device.
%
Proposed and existing quantum devices differ along a variety of axes.
Realistic models of such devices include various restrictions such
as the  limitation to a
fixed number of qubits, a bounded total execution time, or
restrictions on which qubits may interact directly.  
%Looking more closely, 
Primitive operations will require different amounts of time,
different qubit implementations have different failure
modes, be subject to various noise models, and suffer from low fidelity.
\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~\cite{Raussendorf-2001} (\ref{task:mbqc-model}). On one hand,
these models are well understood, stable, and have been extensively
treated in the \zxcalculus literature.  On the other hand, these two
models have different execution concepts and primitive operations,
despite their computational equivalence. They will therefore allow us
to prototype the development of hardware annotations for the \dzxc
system, \newt{cf.\ Task~\ref{task:runnable}}.  In both cases, this
involves three tightly related tasks:
  \begin{enumerate}[label=(\roman*)]
  \item
    decomposing the tensor network into atomic operations;
  \item
    characterising runnability in the model, by predicates in monadic second order logic; and
  \item
    transforming the tensor network into an equivalent runnable version.
  \end{enumerate}
This experience will inform the later work in \ref{wp:theory} and
\ref{wp:usefulstuff}.

To encourage interaction from other research groups, and to support other languages, the interfaces and functionality for the \dzxc system will be made public.
While we will provide specific modules for the tasks described above, the \dzxc system is intended to extensible: therefore we will 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}).
Furthermore, in Task~\ref{task:testBench}, we will develop an open
database of tests, which will serve as a measuring tool for the
quality of the output from the \dzxc compiler.  The database will be made available to the community for rating and testing future compilers or optimisation techniques.

\subsubsection{Representation, reasoning, and resources}
\label{sec:machines-models}

\REM{stuff about WP 2 here}

The purpose of the \dzxc system is to form the basis of a retargetable compiler, able to generate executables for multiple architectures.
We must then develop a way to take into account the different characteristics of these architectures.
The ability to synthesise hardware-appropriate implementations from abstract descriptions is one of the major novel contributions of this project.
\ref{wp:representation} carries out two research avenues towards this objective.

First, we will model the performance characteristics and architectural constraints of various idealised and realistic machines.
We will then develop the means for the \dzxc system to express these properties.
The goal is two-fold: to facilitate code-generation for a given machine from a \zx term; and to expose information needed by the optimiser.

A key research challenge of this first research avenue in \ref{wp:representation} consists in the management of the classical computation and classical information within quantum algorithms.
What computation should occur at the interface between an HLL and the \dzxc system, and which classical parameters are passed on to the \zx terms? Task~\ref{task:betterboxes} focuses on the question of tests based on measurement results: how should they be integrated within the \dzxc system?
While it will already be quite useful to study concrete diagrams of fixed size (e.g.,~a~quantum circuit on $N$ qubits for a previously-fixed $N$) in the early stages of the project,  \newt{Task \ref{task:betterboxes} } %\ref{task:axioms} 
will extend the \dzxc system to support parametrised families of diagrams (e.g.,~quantum circuits with $N$ qubits where $N$ can vary) mirroring the control structures present in a quantum HLL.
This will enable more sophisticated, generic optimisations to be run in advance of needing any particular computational procedure.
The test suite designed in in~\ref{task:testBench} will be used to compare and choose amongst the possible solutions.

In task~\ref{task:axioms}, we will extend the
\zx-calculus in two respects. The first is to expand into complete
and universal qudit variations to work effectively beyond 2-level
systems, and the second is to gain a deeper understanding of the role
played by W-type tensors as they interact with the generators of the
\zx-calculus, which are themselves of GHZ-type. 


The second avenue of research in \ref{wp:representation} tackles a more foundational aspect of quantum computation, pertaining the identification of resources that enable quantum speed-up in computation.
On the one hand, it will use new results on \zx to try to identify what nonclassical aspects of quantum theory serve as a resource.
On the other hand, it will develop procedures to certify whether a quantum algorithm demonstrates speed-up.
This part of \ref{wp:representation} will take a novel\footnote{%
    This work will be novel in the sense that it differs from the traditional approach within the fields of quantum foundations and quantum information theory.
  }
approach to these questions, by tackling them from a \zx-centric perspective.
With this we will further develop the usefulness of \zx as a way in which to describe quantum theory.
This may provide insight on outstanding open problems beyond the scope of the current proposal. 

The question of resources for quantum speedup will be the topic of Task \ref{task:resources}.
Different paradigms of computation, such as Clifford, Clifford+T, and
universal qubit QM, have been recently axiomatised in the language of \zx.
Each of those paradigms, however, offer different degrees of computational power.
By a comparative study of such axiomatic representations, we will aim at identifying, in the \zx language, what is the feature that enables quantum speed-up.
That is, we will characterise quantum resources in a systematic manner using the \zx framework.
By further building a bridge from the \zx formulation and traditional (e.g.,~device independent) approaches to quantum resources, we will be able to contrast our findings with the current intuitions of what may power quantum computing.
These current intuitions include the nonclassical feature of nature called Kochen--Specker contextuality, as well as Bell nonlocality.
Hence, the outcome of \ref{task:resources} will also include the development of \newt{representations} %proofs 
of contextuality within the \zx language.

The certification of algorithms featuring quantum speed-up will be addressed in Task~\ref{task:resourcesagain}.
First, we will identify re-writing processes among the automated theorem proving tools, that cannot be efficiently done with classical algorithms.
This will allow us to identify candidate subroutines that require nonclassical resources to be carried out.
Such subroutines then will be used to develop procedures for characterising if a \zx-represented algorithm demonstrates speed-up. 

\subsubsection{Machine-independent optimisation}
\label{sec:repr-reas-azx}

The formal mechanism which the \dzxc system will use to transform \zx terms (sourced by translation from an HLL)  into optimised, physically implementable computations
are the theoretical core of this proposal.
Developing effective techniques for mapping \zx terms closely to the constraints of hardware is a prerequisite for our success.

We forsee four stages in the compilation process of a \zx
term into instructions for a physical machine.
%The tasks to be performed within \ref{wp:theory} and \ref{wp:usefulstuff} may be broadly described in terms of how the \dzxc system will transform \zx terms produced by the front-end, to obtain instructions to be realised by a quantum computer (or software quantum simulator) at the back-end.
These stages are:
\begin{enumerate}[label=(\roman*)]
\item  
  an initial round of generic, hardware-independent optimisations;
\item
  application of some choice of strategy for error correction;
\item
  translation to a specialised annotation system which represents the parameters and constraints of a specific hardware implementation; and finally,
\item
  a round of optimisation within the constraints of the error correction and hardware models.
\end{enumerate}
The first two stages are machine-independent (\ref{wp:theory}) while the last two are machine dependent (\ref{wp:usefulstuff}).
In addition to the development of the tools for these stages, WP4 will develop an interface for the specification of the annotation systems used in stages (iii) and~(iv) above, allowing for easy extension of the \dzxc system to arbitrary hardware systems, making it suitable for the development of general-purpose quantum compilers.

The first stage of the compilation process represents a ``generic optimisation'' subroutine (\ref{task:basic-opt}), which may be applied to arbitrary \zx terms.
This subroutine will re-write \zx terms into ones with fewer resources in a broadly applicable sense, such as fewer total nodes or fewer nodes which realise non-Clifford transformations (for instance, corresponding to $T$ gates).
This may be developed independently of the results of WP1 or WP2 using existing techniques (as well as incorporating any further useful techniques developed in \ref{task:axioms} and~\ref{task:algorithms}).

Recent breakthroughs in the theory of the \zxcalculus~\cite{Jeandel2017A-Complete-Axio,NW-2018} have shown that whenever two \zx terms describe the same linear operator, then one can be transformed into the other using just a finite set of local, diagrammatic transformations.
However, knowing it is possible
\textit{in principle} to transform one computation (e.g. a quantum
circuit) into another one doesn't say anything about efficiency or our
ability to find effective optimisations. In
Tasks~\ref{task:algorithms} , we will employ theoretical and automated
techniques drawn from rewrite theory to search for better
presentations of \zx terms corresponding to Clifford+T operations, and develop strategies for effectively simplifying \zx terms.
These include Knuth-Bendix completion and theory synthesis.

In Task \ref{task:annotate1}, we will provide the \dzxc system with the ability to express topological constraints and causal ordering.
These could include a restriction to nearest-neighbour interactions for 2-qubit operations on a fixed lattice or enforcing a fixed ordering between two gates.
This will provide us with a test case for more complex annotation systems, such as we will require to treat error corrected systems~(\ref{task:ECC}).

The second stage of the compilation process is to take a generic \zx term expressing a computation on idealised quantum systems, and re-write it as a \zx term representing an equivalent transformation of error-corrected qubits (\ref{task:ECC}).
One of the purposes of ``deep compilation'' of quantum programs is to automatically produce the realisation of the error-corrected form of a procedure.
We have extensive experience in treating error correcting codes in the \zxcalculus
\cite{Duncan:2013lr,Chancellor2016Coherent-Parity,BH-2017,Garvie2017Verifying-the-S}.
Similar techniques will enable translating from ``raw'' \zx terms to error-corrected\,/\,fault-tolerant versions of the same program.
As well as the \zx terms to translate, this will take as input a specification the particular error correction code or other fault-tolerance construction to apply.
Additional annotations will be added to ensure that program transformations performed afterwards do not break the fault-tolerance.

% We identify two kinds of optimisation.
% First, generic, model-independent optimisations work on the raw tensor network, typically by reducing its graph complexity, or by minimising the number of  non-Clifford operations in the graph.
% This draws on \ref{task:algorithms} and could be applied before the target hardwaere is known.


\subsubsection{Machine-dependent optimisation}
\label{sec:comp-quant-softw}


To realise our objective of ``deep compilation'' of quantum programs onto diverse hardware, we must translate the abstractly-described tensor networks represented by \zx terms to optimised code that can run on realistic quantum hardware.
\ref{wp:usefulstuff} concerns this functionality.
This work package represents the most technically involved and multi-disciplinary component of the project, and requires the integration of the front-end \ref{wp:frontend}, the theoretical work of \ref{wp:representation} and instantiation of the generic optimizations considered in \ref{wp:theory}.

We will develop a further layer of annotations for \zx terms, to provide a means for the \zxcalculus to respect real-world constraints coming from quantum hardware.
This annotation system will again be modular, in that any hardware platform may be described by an annotation system independently of other platforms.
This will make the \dzxc system extensible in principle to any sufficiently well-characterised quantum computing platform.

Annotation systems representing the hardware implementation are to be provided by the development environment, using a standardised interface, as developed in \ref{task:backendapi}.
As a way to demonstrate and to prototype this hardware-dependent annotation layer,  we will study concrete hardware platforms quantum computers based on different technologies: silicon spin qubits (Grenoble) in Task~\ref{task:qdot-model}, and optically linked ion traps (NQIT) in Task~\ref{task:NQIT-model}.
In both cases we will interact strongly with the experimental groups working on these
models, who are close colleagues of our consortium members (D.~Horsman for Grenoble, and N.~de Beaudrap for NQIT).
Since these architectures are dissimilar, tackling both is an ideal demonstration of our approach. 
The completion of this phase will allow quantum programs
generated by the \dzxc system
to be run on real hardware.

The final, machine-dependent part of the compilation process consists of two stages: formatting to the target system (\ref{task:runnable}) and a last round of machine-dependent optimizations (\ref{task:opt-machine}).
We identify three main tasks:
  \begin{enumerate}[label=(\roman*)]
  \item  
    to add suitable machine-dependent error protection to the program;
  \item
    to optimise the program according to whichever resources are most appropriate for the given machine; and
  \item
    to lay out the program for execution.
    \end{enumerate}
Although we treat them separately, in practice these tasks
will interact in non-trivial ways, and their order need not be fixed.

The annotation system overlays the abstract rewrite theory of \zx-diagrams with real-world constraints coming from quantum hardware.
We will then develop the formal tools for rewriting \zx-diagrams in ways that
respect those constraints. 
In task \ref{task:annotate2} we will explore methods to annotate a \zx-diagram with quantitative information such as timing, noise, or fidelity.
In real-world systems, these can vary vastly between qubits interacting in different ways (e.g.,~neighbouring in ion trap vs.\ interactions mediated by optical channel~\cite{PhysRevX.4.041041}) or stored in different physical modes.

The third stage of the compilation process attempts to map a \zx term into an equivalent \zx term which closely models the constraints of a target architecture (\ref{task:runnable}).
This represents the core of the compilation process, taking \zx terms representing a procedure in an abstract model of quantum computation such as circuits or MBQC patterns (with or without error correction), and mapping them into a form which conforms to the physical constraints of a specific hardware implementation.
%Particular implementations are specified by a system of annotations provided by the development environment, consisting of an ``architecture-targeted annotation'' (or ArcTAn) system.
%ArcTAn systems will generalise the particular examples of implementation-oriented annotation systems developed in \ref{wp:representation}, and will aim to encompass as many extant and forseeable quantum hardware platforms as possible, incorporating topological and time-ordering constraints as captured by the results of \ref{task:annotate1}.

The fourth and penultimate stage of the compilation process --- prior to emitting instructions in the machine language(s) of the target hardware --- is a final round of optimisation, which this time respects the constraints of the specific choice of error correction strategy and machine resources specified by the input~(\ref{task:opt-machine}).
%This will involve the development of a theory of re-writing techniques developed in \ref{task:annotate1} to ArcTAn annotation systems.
%By performing a final round of optimisations using a theory of rewrites which apply to all ArcTAn annotation systems, we aim to 
This will make possible a reduction in the resources used in any particular hardware platform without requiring the use of bespoke techniques for each target architecture.


\subsection{Interdisciplinary nature}
\label{sec:interd-nature}

As shown the schema at the beginning of \S\ref{sec:summary:-}, 
the ambitious vertical structure of this project requires a uniquely
diverse range of expertise: from \textbf{Software Engineering \&amp; Formal Methods} at the high level, through \textbf{Quantum Computation} and logic at the mid-level, down to quantum \textbf{Systems Architecture} at the low-level.
This project unites those working in quantum information theory from logical and pure mathematical perspectives with those working on practical error correction, quantum
hardware, and more generally programming language
design and system engineering.
It thus provides a unique opportunity for theoretical insight to inform future technology, and for technological problems to drive future theory.
We will promote these cross-disciplinary interactions by a number of our planned activities, including holding a summer school which will provide both introductory tutorials and more advanced material on the range of techniques and methods which will be used and developed in the project, in a form accessible to both computer scientists and physicists from a wide range of backgrounds. 


\newpage

\section{IMPACT \REM{(1 page -- this is shorter than long proposal)}}
\label{sec:impact-2-pages}

\subsection{Expected impacts}
\label{sec:expected-impacts}
%% maybe turn \subsections into \paragraphs to save space?

\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.}

DZXC significantly advances the state-of-the-art across six of the seven expected impacts.

The project will \textbf{develop a deeper fundamental and practical understanding} of systems for quantum information processing.
We will develop a deep quantum compiler that can take input in a variety of high-level quantum programming languages, automatically add error correction, optimise the process, and output machine instructions adapted for different quantum devices.
Creating the system necessarily will produce foundational insights into the operation and capability of quantum devices including using the \zxcalculus to identify and certify resources required for quantum speedup.
The \dzxc system will model noise, error rates, and connectivity of the target platforms and take steps to minimise decoherence, thus \textbf{enhancing the robustness and scalability} of quantum information technologies.

As the basis of a retargetable compiler, the \dzxc system will make it easy to support new quantum devices and thereby \textbf{identify new opportunities and applications} fostered through quantum technologies.
By providing open APIs, we will make the \dzxc system available to all academic and industrial users, thus \textbf{transferring these technologies} from laboratories to industries.
The intelligent compilation chain will make quantum programming available to non-specialists, \textbf{enlarging the community involved} in tackling the new challenges of quantum computation.
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 on to formal methods of computer science, which \textbf{enhances interdisciplinarity} and \textbf{crosses traditional boundaries} between disciplines.

With our newly-founded member group at the University of Gdansk, we have a \textbf{partner from the widening countries}.
The project also involves several other research groups that have been founded in the past few years, thus \textbf{building leading innovation capacity}.
Additionally, the team includes as co-investigators multiple \textbf{excellent young researchers} on the brink of group development.
Our industrial partner, CQC, is an \textbf{ambitious high-tech SME} with a team leader who has expertise in technology transfer from academia to industry.


\subsection{Dissemination, exploitation of results, communication}
\label{sec:diss-expl-results}

\REM{Provide a plan for disseminating and exploiting the project results beyond the project itself.  
Results include any data produced in the framework of the project. If applicable, describe how data curation and distribution can be ensured beyond the project duration. 

Describe the proposed communication measures for promoting the project and its findings during the period of the project. Measures should be with clear objectives. They should be tailored to the needs of different target audiences, including groups beyond the project’s own community. 
Where relevant, include measures for public/societal engagement on issues related to the project.}

\paragraph{Dissemination.\!\!}
\label{sec:dissemination}
%\bR personal opinion : we should be bold and say Fuck the (journal)
%System.  We will publish only in true open venues like Quantum.
%Nature can go to hell. \e
The primary means of dissemination will be by publishing our results
in leading journals and conferences, with a strong preference for open access
venues.  (We note that in computer science, the highest impact
publication venues are conferences with published proceedings.)  
%We will target: 
\begin{itemize}
\item Specialist quantum information venues: \emph{Quantum Information
    and Computation} (QIC), \emph{Quantum Information Processing}
  (QIP), \emph{Theory of Quantum Computation} (TQC), and \emph{Quantum
    Physics and Logic} (QPL). 
\item Mainstream computer science venues: the \emph{Journal of the 
    ACM} (JACM),
    the \emph{International Conference on Computer-Aided Design} (ICCAD), \emph{Logic in Computer
    Science} (LiCS), \emph{Principles of Programming Languages}
  (POPL), \emph{Automata, Logic and Programming} (ICALP), \emph{Tools
    and Algorithms for the Construction and Analysis of Systems}
  (TACAS). 
\item Mainstream physics journals: \emph{Physical Review Letters} (PRL),
  \emph{Physical Review A} (PRA), the \emph{New Journal of Physics} (NJP), and
  \emph{Communications in Mathematical Physics} (CMP), 
  \item \newt{The diamond open access journal \emph{Quantum}.}
  \item \newt{Our own recently
  established diamond open access journal \emph{Compositionality}.}
\end{itemize}
The consortium members have a strong record of publishing in all of these
leading venues.  %Other venues will targeted opportunistically in order to achieve the most timely publication of our results.
\newt{However, as strong supporters of (diamond) open access publishing, we feel strongly about publishing in the latter two, as well as the other open access journals.}

We plan three annual workshops, which will
be open to any interested parties.  The final workshop will include a
school aimed at PhD students and potential end-users in industry.  We
allocate significant budget for student bursaries to maximise
participation.

\paragraph{Exploitation of results.\!\!}

We propose several direct and indirect routes to exploitation of our
results.  Firstly, our consortium includes an industrial partner, CQC,
and \newt{a key member} of the NQIT project (de Beaudrap).

Though CQC our research will be integrated with the leading quantum
software compiler system, \tket.  Since \tket already incorporates
ideas from the \zxcalculus this offers a direct and natural route to
exploitation. Further, since \tket already supports several existing
software frameworks, and several hardware platforms, this promotes the
widest possible uptake of the project's results by end users, for no
additional work by the project members.  To ensure a strong
relationship between CQC and the academic partners, the Oxford-based
post-doc will spend approximately 25\% of their time on site at the
CQC offices in Cambridge.


\newt{With NQIT, we will provide a programming framework for the networked quantum computer developed as part of that project (and the quantum computing project which follows afterwards in Phase~II of the UK Quantum Technologies Programme), seek to collaborate with their architectures team, and present the project results at the UK Quantum Technologies annual showcase.

In both cases, our work can be exploited
directly by end-users.} %% copied from Niel's document so I assume this is up-to-date

\TODOb{This para to be cut.}
\bR In addition, we have also recruited a board of advisers (see below)
including the European leaders in scalable quantum devices.  These
experts will participate in our annual workshops to help define
requirements and ensure that our work can be used by their projects.
The DiCarlo group (Delft) and Rigetti have shown particular interest
in exploiting our work to assist with supporting the superconducting
quantum devices they are developing. \e

\newt{Finally, we commit to produce public APIs (see
\ref{del:frontendapi}, \ref{del:backendapi} and \ref{del:backendapiBIS})
for the \dzxc system which will allow any programming language to
generate code using our system, and make it easy to add support for
future hardware targets.  This will enable other projects to
integrate \dzxc into their system.  To further advance this aim, the
software tools developed by our project will be released on an
open-source basis with a permissive license (See
\S~\ref{sec:cons-agre}.) }

\paragraph{Communication.\!\!}

%To communicate of our work to a wider audience, and to take advantage
%of wide public interest in quantum technology, we will perform a
%variety of outreach activities.  Firstly, we will adopt ``open
%lab-book'' research, publishing work-in-progress on a project wiki,
%and articles aimed at a general audience on a project
%blog.\footnote{The success of \emph{Graphical linear algebra}
%  (\href{http://graphicallinearalgebra.net}{\color{blue} graphicallinearalgebra.net}, 217K visitors since 2015) demonstrates there is a clear audience for such works.}
%%To allow end-users to experiment with \azx, Bull will
%%provide an HPC simulator with a publicly accessible front end, which
%%will also be incorporated into the project website.

Beyond online self-publishing we will also pitch articles to magazines 
aimed at a general audience in several languages.  We will
specifically target:
\begin{itemize}
\item English: \emph{Communications of the ACM}, \emph{IEEE Computer},
  \emph{Physics Today}, \emph{Nautilus}, \emph{Quanta}, \emph{Aeon},
  \emph{Ars Technica}, \emph{New Scientist}, \emph{FQXi blog}.
\item French: \emph{La Recherche}, \emph{Pour la Science}, and
  \emph{Interstices}.
\item \bR Dutch: \emph{Kijk Magazine}, \emph{Quest}, and the dutch edition
  of the \emph{New Scientist}.\e \TODOb{replace dutch ones?}
\end{itemize}
Several of members of the consortium have had their work featured in
these publications before.  
%In addition, the \azx system itself will
%also be routinely presented in any industrial or public engagement
%events which touch on the software tools used by NQIT.

\paragraph{Advisory Personnel:\!\!} 
\label{sec:advsiory-board}

In order to ensure the maximum impact, and to complement the expertise
present in the consortium, we have recruited additional
advisors who will consult with the project.
\begin{itemize}
\item \textbf{Prof. Alexia Auffeves} is the Lead scientist of the
Grenoble Quantum Engineering project
\item  \textbf{Prof. Maud Vinet} is the head of the silicon spin qubit experimental team
\end{itemize}
Letters of support from are attached at the end of
this document.

\newpage
\section{IMPLEMENTATION \REM{(2 pages total -- shorter than long proposal)}}
\label{sec:impl-2-pages}

\subsection{Work plan} \label{sec:work-plan-work}

\REM{Provide a brief presentation of the overall structure of the work plan.
Clearly define the intermediate targets. 
Provide a timing of the different work packages and their components
(Gantt chart or similar). 
Provide a graphical representation of the work packages components
showing how they inter-relate (Pert chart or similar).
}

The work plan has four major scientific work packages (WPs),
%each focusing on a different \emph{theme} within the project.  The work packages
which will proceed in parallel.
All will have at least some activities throughout the length of the project, with the exception of \ref{wp:usefulstuff} which builds on earlier work in the other WPs and thus only begins one year into the project. (There is also a fifth
work package grouping administrative and organisational activities.)
\begin{description} 
\item[\ref{wp:frontend}] is focussed on \newt{the \dzxc interface with known high-level quantum programming languages} 
%translating from HLLs into \azx, reflecting higher level programming constructs into \azx, 
and building a test suite of programs \newt{for benchmarking}.
\item[\ref{wp:representation}] \newt{is focussed on the further development of zx calculus, its axiomatic formulation, and its status as a theory of resources.}
%is about modelling the properties of different machines in \azx, and translating \azx to hardware.
\item[\ref{wp:theory}] 
\newt{focusses on resource optimization, such as gate reduction in circuit representations, efficient intelligent error-correction, and other deep algorithms.}
%develops the theory behind \azx and algorithms  to realise the logical ideas.
\item[\ref{wp:usefulstuff}] 
\newt{applies all the previous to specific quantum hardware.}
%applies these advances to the
%creation of useful quantum software, specifically focusing on
%optimisation and error correction.
\end{description}
Each work package is divided into more specific tasks, each of which 
is designed to deliver a particular piece of the project: some are
theoretical results, some are software functions.  Broadly speaking,
the tasks are sequenced in order of technical difficulty so that
experience gained on earlier tasks can be applied to the more
difficult ones.  There are strong interactions between the tasks, and
early outputs of each WP will be used in later outputs of other WPs.
(Details about the tasks are found in \S~\ref{sec:work-packages}.)

\begin{figure}[th]
  \centering
  \makebox[\textwidth][c]{\input{ganttchart.tex}}
  
  \caption{Approximate timings and durations of tasks (months)}
\label{fig:gantt}
\end{figure}

%%%%%%%%%%%%%%%%%%%%
%% Overall structure
%%%%%%%%%%%%%%%%%%%%

The project is a single integrated whole, so there are many linkages
between the work packages; these are displayed in
Figure~\ref{fig:pert}. As discussed in
\TODOb{I don't think this is actually discussed in \S~\ref{sec:manag-struct-milest}}
\S~\ref{sec:manag-struct-milest}, only some of these linkages are true
dependencies, where later tasks rely on results of earlier ones. On the other hand, many tasks can influence and enhance each other as they run in parallel. 

Our work plan consists of a balance of short tasks with concrete software deliverables (e.g. \ref{task:circuit-model}, \ref{task:mbqc-model}) and longer term, more ambitious and open-ended tasks (e.g. \ref{task:algorithms} and \ref{task:opt-machine}) which can offer significant, but less predictable, step-changes in the state of the art.

Several tasks of \ref{wp:frontend} are ``long and thin'': that is, they are intended to work in parallel with the other WPs, with new features being integrated as they are developed.
Similarly, much of the theoretical work in \ref{wp:representation} and \ref{wp:theory} is intended to be developed alongside the more implementation-oriented WPs.
These theory-oriented WPs will draw inspiration from the practical ones and feed back into them in turn.

The early tasks of \ref{wp:frontend} are quite
practical and don't require much preparation to begin. They will provide
useful experience for the later tasks.
The first three tasks of \ref{wp:representation} build on a significant existing body of results and techniques for the \zxcalculus and quantum information theory.
Similarly, several tasks of \ref{wp:theory} are based on known results and techniques for the \zxcalculus and rewrite theory in general.
Hence, they can begin immediately.
This will provide an ample source of theoretical work to do until the more implementation-oriented tasks \ref{task:circuit-model} and \ref{task:mbqc-model} provide enough examples and use cases to feed into tasks \ref{task:resourcesagain},  \ref{task:annotate1} and \ref{task:annotate2}.

The more challenging machine models of \ref{task:qdot-model},
\ref{task:NQIT-model} and \ref{task:IBM-model} are scheduled to begin in parallel with the more challenging theoretical tasks in \ref{wp:theory}, anticipating a great deal of back-and-forth interaction between these two aspects of the project.
\ref{wp:usefulstuff} requires integrating and generalising many of the 
ideas of \ref{wp:representation} and \ref{wp:theory}, so it is mostly
scheduled toward the end of the project.

\TODOb{update pert chart}
\begin{figure}[h]
  \centering
  \input{pertchart.tex}
  
  \caption{Dependencies and interactions between tasks} 
\label{fig:pert}
\end{figure}

%%%%%%%%%%%%%%%%%%%%%%%
%% Intermediate targets
%%%%%%%%%%%%%%%%%%%%%%%
Our intermediate targets are described in the deliverables of each WP and in the milestones in \S~\ref{sec:manag-struct-milest}, with the latter focussed towards providing working pieces of software.
On the theory side, we aim to augment the \zxcalculus in several directions: by going from qubits to qudits (\ref{del:qudits}), developing representations for recursion and control (\ref{del:recursion}), and expressing topological and causal constraints (\ref{del:topology}).
Throughout the project, we will check the performance of our methods against competitors (\ref{del:outperform}) and benchmark our software using the open test-suite we will develop (cf.\ \ref{task:testBench}).


\TODOb{is this paragraph needed/needed here?}
The allocation of staff to work packages is discussed in
\S~\ref{sec:consortium-as-whole} and \S~\ref{sec:descr-cons}.
However, because of the integrated nature of the project, and the high 
degree of past collaboration among the consortium members, most tasks
receive attention from the personnel of several sites.  This degree of
collaboration is a strong point of this project.

\newpage

\def\partnerref#1{{\hypersetup{hidelinks}\ref{#1}}}
  


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\input{old-wps.tex}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newpage
\paragraph{Work package overview}
\label{sec:work-pack-overv}

\newt{\begin{center}
  \begin{tabular}{|p{0.2\textwidth}|c|c|c|c|c|c|}
    \hline
    \textbf{Partner} 
    &amp; \ref{wp:frontend} 
    &amp; \ref{wp:representation} 
    &amp; \ref{wp:theory}
    &amp; \ref{wp:usefulstuff} 
    &amp; \ref{wp:admin} 
    &amp; \textbf{TOTAL} \\\hline
1. Grenoble   &amp;  12 &amp; 2 &amp; 12 &amp; 20 &amp; 3  &amp; 49 \\\hline
2. LORIA      &amp; 20 &amp; 12 &amp; 9  &amp; 9  &amp; 3  &amp; 53 \\\hline
3. Oxford     &amp; 32 &amp; 14 &amp; 30 &amp; 12 &amp; 2  &amp; 90 \\\hline
4. CQC        &amp;  4 &amp; 0  &amp; 6 &amp;  2 &amp; 0  &amp; 12 \\\hline
5. Gdansk     &amp;  12&amp; 42 &amp; 12 &amp; 6 &amp; 4  &amp; 76 \\\hline
6. Nijmegen   &amp;  3 &amp; 6  &amp; 12 &amp; 0 &amp; 0  &amp; 21 \\\hline
\textbf{TOTAL}&amp; 83 &amp; 76 &amp; 81 &amp; 49 &amp; 12 &amp; 301   \\\hline 
  \end{tabular}
\end{center}}

\REM{(total effort per WP and partner in person.months)}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newpage
\subsection{Management structure, milestones, risk assessment}
\label{sec:manag-struct-milest}

\REM{Describe the organisational structure and the decision-making. 
\textbf{including a list of milestones (template provided). A
  milestone is a major and visible achievement. It should be SMART:
  Specific, Measurable, Attainable, Relevant, Time-bound.}
Explain why the organisational structure and decision-making
mechanisms are appropriate to the complexity and scale of the
project.}

\paragraph{Coordinator}
\label{sec:overall}

Coordination between sites and between work packages will be overseen
by D. Horsman at the Grenoble site, which will also handle the
overall administration of the project.

\paragraph{Sites}
\label{sec:sites}

The project will be managed by a senior scientist from each site: 
B. Coecke (Oxford), R. Duncan (CQC), D. Horsman (Grenoble), A. B. Sainz (Gdansk),
S. Perdrix (LORIA), and A. Kissinger (Nijmegen).  They will track
global progress to ensure milestones are reached, and facilitate
collaboration across tasks at their individual sites. They will be in close contact throughout the project to assure coherence and concurrence of the activities at the different sites.

\paragraph{Work packages}
\label{sec:work-packages-1}

Each work package will be lead by a responsible PI who will coordinate
research activity between sites to ensure that deliverables are met,
achieve WP-specific objectives, and organise collaboration meetings as
needed.  
\textbf{\ref{wp:frontend}}: S. Perdrix (LORIA), 
\textbf{\ref{wp:representation}}: A. B. Sainz (Gdansk),
\textbf{\ref{wp:theory}}: B. Coecke (Oxford),
\textbf{\ref{wp:usefulstuff}}: D. Horsman (Grenoble),
\textbf{\ref{wp:admin}}: D. Horsman (Grenoble).

\paragraph{Experimental and integration advisory board}
\label{sec:monit-advis-board}

Every six months there will be a meeting of both the work package leaders
and the site leaders, either electronically (\eg via Skype) or at a 
project event.  At these meetings progress towards research objectives
will be evaluated, and any new opportunities will also be discussed.  These
meetings will be organised by the coordinator.  

To assist in monitoring and evaluating progress, as well as to collaborate on WP4,
we have recruited Alexia Auffeves and Maud Vinet as external advisors. Prof. Auffeves is the Lead of the
Grenoble Quantum Engineering project, and Prof. Vinet is the head of the silicon spin qubit experimental team.
The entire project and advisory board (see \S\ref{sec:impact-2-pages})
will meet once a year to evaluate progress, set priorities, and plan
next steps.


\bR
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\paragraph{List of milestones}
\label{sec:list-milestones}

The milestones of the project are conceptually simple: at each
milestone we will deliver a functioning piece of software.  With each
milestone, we add more, and more advanced, functionality.  By
delivering the software incrementally, we follow best practice in the
industry:  by regularly integrating parts from all work packages, we
reduce risk and improve communication across the consortium.  

\begin{center}
\makebox[\textwidth][c]{
  \begin{tabular}{|c|c|c|l|}
   \hline
    \textbf{Milestone} &amp;
    \textbf{Delivery Month} &amp;
    \textbf{WP involved} &amp;
    \textbf{Title} \\\hline
%
\ms \label{ms:qasmqasm}&amp;
12 &amp;
\ref{wp:frontend}  &amp;
Minimal QASM $\to$ QASM circuit optimiser \\\hline
%
\ms \label{ms:quippermbqc}&amp;
18&amp;
\ref{wp:frontend},\ref{wp:representation},\ref{wp:theory}&amp;
Support for one HLL using parametric \zx,\\
&amp;&amp;&amp; with 1WQC and idealized circuit output \\\hline
%
\ms \label{ms:optimise-ecc}&amp;
24&amp;
\ref{wp:representation},\ref{wp:theory},\ref{wp:usefulstuff}&amp;
Architecture sensitive, fidelity aware optimiser\\
&amp;&amp;&amp; Error correction support
 \\\hline
%
\ms \label{ms:nqitbackend}&amp;
30&amp;
\ref{wp:frontend},\ref{wp:theory},\ref{wp:usefulstuff}&amp;
 Back-end support for Oxford Ion Traps,\\
 &amp;&amp;&amp; initial back end API\\\hline
%
\ms \label{ms:delftbackend} &amp;
36&amp;
All&amp;
Complete deep-\zx compiler stack with open\\
&amp;&amp;&amp; APIs, and a target compiled protocol\\
&amp;&amp;&amp; demonstrating explicit quantum speed-up. \\\hline
  \end{tabular}}
\end{center}

\e



\paragraph{Critical risks for implementation}
\label{sec:crit-risks-impl}


\REM{Describe any critical risks, relating to project implementation, that
the stated project's objectives may not be achieved. Detail any risk
mitigation measures.\textbf{Please provide a table with critical risks
  identified and mitigating actions (template provided).}
}


The project is overall quite high-risk, in the sense that what we
propose is in the most part entirely novel, and might fail.  The
rewards for success would be correspondingly great.  However, we have
designed the project to survive the failure of many (or even most) of
its tasks and still deliver value.

We mix low and high risk activities.  Success in low
risk activities (\ref{task:trans1}, \ref{task:basic-opt}, \ref{task:ECC},
%\ref{task:axioms}, THIS IS NOT REAALY LOW RISK
\ref{task:circuit-model}, \ref{task:mbqc-model})
will still deliver significant progress towards our overall objective.
\oldt{\ref{wp:theory} is the most critical; here we mitigate the risk by
(i) developing experience on easier objectives before addressing more
demanding ones and (ii) consulting our board of advisors to foresee
problems.  Due to its high dependence on other tasks, we consider
\ref{wp:usefulstuff} to be highest risk.}\TODOb{This doesn't seem quite up-to-date, also see below}



\begin{center}
  \begin{tabular}{|p{0.25\textwidth}|c|c|p{0.4\textwidth}|}
    \textbf{Description of risk} 
    &amp; \textbf{Likelihood}
    &amp; \textbf{WPs involved}
    &amp; \textbf{Proposed mitigation measures}\\\hline
%    
Can't hire suitable post-docs&amp;
Medium&amp;
All&amp;
While we have already identified several suitable candidates for each
role, the investigators also collectively supervise a large body of PhD
students and post-docs who could be channelled to the project.
\\\hline
%    
NQIT or Grenoble machine info unavailable or not detailed enough&amp;
Low&amp;
\ref{wp:usefulstuff}&amp;
\oldt{(i) We have members of the consortium from NQIT, and letters of
support from DiCarlo who agrees to help.  (ii) We can approach other
members of our board of advisors, or other friendly
experimentalists. (iii) We can target an more abstract model of the
machine} \\\hline
%    
Some desired technique or algorithm isn't found&amp;   
High&amp;
All&amp;
All tasks where this is a risk have been structured as a collection of
related goals; if some part doesn't succeed then the finished system
will be will have fewer features, or worse performance.  However it's
very unlikely that an entire task will fail in a way that jeopardises
the project. \\\hline
%    
Software integration issues&amp;
Medium&amp;
All&amp;
(i) We will establish a common API in \ref{del:earlyapi} to allow
loose coupling of the software components (ii) We appoint the most
experienced software developer in the  consortium (Valiron) to act as ``integration tzar'' and ensure
the global design is good. (iii) As noted above, we will integrate
often and deliver new features more than once a year.  
\\\hline
  \end{tabular}
\end{center}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newpage
\subsection{Consortium as a whole} %\REM{(1 page)}
\label{sec:consortium-as-whole}

%%\REM{The individual members are described in section 3.5, there is no
%  need to repeat that information there.  
%Describe the consortium. How will it match the project's objectives
%and bring together the necessary expertise? How do the members
%complement one another? 
%In what way does each of them contribute to the project? Show that
%each has a valid role and adequate resources in the project to fulfil
%that role. 
%If applicable, describe the industrial/commercial involvement in the
%project and explain why this is consistent with and will help to
%achieve the specific measures which are proposed for exploitation of
%the results of the project.  
%}

\newt{The members  of the consortium are chosen to provide the best 
combination of skills to deliver this project, including the fathers of  \zxcalculus, those who established it as a universal and complete calculus, those who have developed applications of \zxcalculus to quantum technologies, and those who have outperformed all other methods using \zxcalculus.      
%They also contributed greatly to community building. 
 
\TODOb{Do we think it's really good to say we are the Oxford mafia?
  Also i had two other positions between Oxford and CQC -rd}
Many members also have a long history of collaboration, and in fact have been at different consortium sites at some point of their career, for example Wang was a postdoc at Nancy before moving to  Oxford and CQC. Duncan,  Horsman, Kissinger and Perdrix were postdocs at Oxford before moving to CQC, Grenoble, Nijmegen and Nancy respectively. Sainz has a long-standing collaboration with members of the Oxford Group, and organised Quantum Physics and Logic X, the main conference for \zxcalculus alike research, while at Barcelona.  Coecke is a member of the International Scientific Committee of ICTQT-Gdansk, the new institute that hosts Sainz' new group.

Several members have ongoing collaborations with Cambridge Quantum Computing Inc. In particular, co-inventor of \zxcalculus Ross Duncan is now the leading researcher at CQC, which clearly demonstrates CQC's commitment to \zxcalculus.  Quantum compilation  is moreover the key focus of CQC. Several members are  part of the NQIT Quantum Technologies Hub.\footnote{nqit.ox.ac.uk}   

%We now provide details on each of these.

Expertise on the
{\bf theoretical aspects} underpinning the project is provided by Oxford site leader Coecke and CQC research leader Duncan 
 who jointly invented the \zxcalculus\  \cite{Coecke:2009aa}. Backens, Perdrix, Jeandel and  Wang are the key  contributors to establishing universal completeness of \zxcalculus \cite{1367-2630-16-9-093021, Jeandel2017A-Complete-Axio, HFW}. Coecke pioneered general categorical and diagrammatic methods in quantum computing \cite{AbrCoe:CatSemQuant:2004}, and with Kissinger co-authored the textbook of the field \cite{Coecke2017Picturing-Quant}.
 
Expertise on {\bf quantum technology applications} is provided by those who pioneered these applications.  Duncan, Perdrix and Horsman  pioneered zx-based translations  between different computational models \cite{Duncan:2010aa, Horsman:2011lr}, Horsman and Kissinger pioneered zx-based error-correction  \cite{Chancellor2016Coherent-Parity}, and Horsman and de Beaudrap  demonstrated the equivalence of zx-rules and lattice surgery \cite{BH-2017}. 
 
Duncan and Kissinger  pioneered {\bf automation} of diagrammatic reasoning (cf.~{\tt quantomatic} and {\tt PyZX}), which also will play a key role in this project, as they already have in setting the state-of-the-art in circuit optimization \cite{DKPdW-2019}.    

We also  include pioneers in {\bf quantum
programming languages} (Valiron), important contributors to the 
theory of {\bf MBQC} (Perdrix, de Beaudrap, and Duncan) and 
{\bf quantum circuits} (Jeandel).  }  

The consortium has also been instrumental in community building, for example with the QPL conference series which now attracts well over 100 participants every year and approx.~75 paper submissions on foundational and structural research in the area of quantum computing.  It also has organised several schools e.g.~the QiCS School\footnote{www.cs.ox.ac.uk/people/bob.coecke/QICS$\underline{\ }$School.html} and the CAP Spring School,\footnote{www.cs.ox.ac.uk/ss2014/} and a substantial talks archive is maintained.\footnote{www.youtube.com/user/OxfordQuantumVideo} \newt{More recently, the several members are 
involved in the Compositionality community, which has diagrammatic/categorical reasoning as its core focus, with a new journal, a new conference series, and a new workshop series.}

\TODOb{Keeping any of this? Introducing anything else?}
\bR Of utter importance is the alignment with Networked Quantum Information Technologies Hub (NQIT) at the Oxford site, which means that several members of the consortium have already direct expertise with interacting with quantum hardware (de Beaudrap, Horsman).  The NQIT is the largest of the four Hubs in the UK National Quantum Technology Programme, a 270 GBP million investment by the UK government to establish a quantum technology industry in the UK. %We are working towards building a quantum computer demonstrator, the Q20:20 engine, which demonstrates a networked, hybrid light-matter approach to quantum information processing.
Concretely, 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 \zx-operations \cite{{BH-2017}}. This will certainly make the ambition here much more achievable. \e

%\REM{From cyril to address industrial/commericial}
%Bull brings expertise in high performance simulation as well as
%industrial guidances in software. \REM{more}



\newpage%\TODOb{This needs to be done urgently}
 \subsection{Financial plan}
\label{sec:financial-plan} 

\REM{The resources to be committed for each project partner have to be
  described in the Electronic Submission System by the
  coordinator. These resources include: Personnel, Consumables,
  Equipment, Travel, Subcontracting, Provisions, Licensing fees,
  other. Justify them here. Both the justification and the information
  in the system will be communicated to the Evaluation Panel.}

\paragraph{Personnel} 
\label{sec:personnel}

This is a large and multifaceted project, which will require
significant work to deliver.  A full-time post doc at each contributing academic
site is needed, under supervision of the site lead.  In addition, At
all the academic sites there is a large amount of time donated to the
project by senior scientists with relevant expertise.  At CQC, our
industrial partner, a Senior Scientist and a Research Software Developer will contribute to the project.

\begin{itemize}
\item \emph{Post-doctoral researchers}: We request 30 months of salary
  for post-docs at Oxford, 36+18 months at Gdansk, and 18 months at each of Grenoble and LORIA. The Oxford post-doc will also engage in co-operation with industrial partners at CQC.  The post-docs
  will be hired as soon as possible by the site leads at each site.
%\item \emph{Coordinator}: We request 10\% contribution the
%  Duncan's salary at Strathclyde to cover the time spent managing
%  the project. This is reduced from 20\% upon negotiation with
%  Stratclyde.  (Duncan will contribute an additional 8.4 months of
%  time as a researcher, see below.)
\item \emph{Principle investigators and other named staff}: Spread
  across the sites, more than 110 person-months of time
  will be contributed by the named staff on the project, all of which
  is supported by other sources.  This means that almost 40\% of the
  research effort of the project is funded from elsewhere.
\item \emph{PhD Students}: at LORIA, Titouan Carette will contribute
  approx 9 months to the project; this is funded from other sources.
  At Grenoble, Richard East will contribute
  approx 9 months to the project; this is funded from other sources.
  At Gdansk, a PhD student will contribute
  approx 12 months to the project; this is funded from other sources. \newt{At Oxford, at least two PhD students will contribute to the project, as well as several MSc students}.
\item \emph{Engineers}: At CQC, a Senior Scientist and a Research Software Developer will contribute, funded from other sources.
\end{itemize}

\paragraph{Workshops}
\label{sec:workshops}

Project workshops serve a key role in intra-project communication,
dissemination, and outreach.  We plan one workshop each year, in
Oxford, Nijmegen, and Grenoble.  We plan to invite significant figures from the experimental and software industrial communities to supplement the project reach and expertise, which increases the cost beyond
the usual expenses of venue hire and speakers' expenses.  We have
budgeted
\euro 15k for each, through the co-ordinating site budget.

\paragraph{Travel and subsistence} 
\label{sec:travel-subsistence}

Since many of the personnel have expertise relevant to more than one
work package, we request substantial budget for travel, for quantERA
reporting meetings, for formal project meetings, smaller more frequent
WP meetings, and also to present our work at conferences.

\paragraph{Equipment}
\label{sec:equipment}

\begin{itemize}
\item We  request laptop computers for each of the postdocs, and
  replacement laptops for some staff.  These are necessary
  because of the frequent need to travel and work at another site
  and/or present work at conferences or workshops.
\end{itemize}

\section{ETHICAL ISSUES \REM{1/2 page}}
\label{sec:ethical-issues}

\REM{Describe any foreseeable ethical issue that may arise during the
  course of the research project. Describe all mitigation strategies
  employed to reduce ethical risk, and justify the research
  methodology with respect to ethical issues.}

No ethical issues foreseeable.

\REM{max 30 references - OK AT THE MOMENT SINCE KEVIN-ROSS ONLY IN COMMENTS}
\bibliographystyle{plain}
\bibliography{quantera} 

\end{document} %%% -- uncomment to throw away notes

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
</pre></body></html>