SHORTPROP.tex

% !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}\vspace{-1.5mm}%suck
\label{sec:targ-breakthr-basel}

\REM{\vspace{-1.5mm}%suck
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.\vspace{-1.5mm}%suck

%\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 
  allow for easy, customisable cross-compilation; no such tools exist for quantum devices.
  Optimisation, in particular around error correction, will be vital for running post-classical protocols on near-term hardware. Classically, this is part of an integrated compiler.
  Quantum technologies will continue to be scarce and valuable; identifying truly quantum resources (beyond 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 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.\vspace{-1.5mm}%suck
  

\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-diagram4.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:\vspace{-1mm}%suck
  \begin{itemize}
  \item
    incorporating architectural constraints
  \item
    optimising resource use
      \item
    certifying speed-up
  \item
     managing error correction.    \vspace{-1mm}
  \end{itemize}
These will be specified in a modular way but tightly integrated upon compilation.
  %To demonstrate this technology, w
  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.\vspace{-1.5mm}%suck
  

%  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}.
    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 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 modern compiler.
  
  To build comparable quantum compiler technology we use the \zxcalculus, %has been extensively applied to quantum computation, and
  a formal system for transforming quantum procedures in a way that preserves meaning.
  It 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}.
Powerful and flexible, the \zxcalculus can easily describe computations in both the circuit and measurement-based models of quantum computation (MBQC)~\cite{Raussendorf-2001,DanosV:meac,Duncan:2012uq,Duncan:2010aa} and can formulate and verify quantum error correcting codes \cite{Horsman:2011lr,Chancellor2016Coherent-Parity, Duncan:2013lr} and quantum algorithms \cite{Stefano-Gogioso2017Fully-graphical, Zeng2015The-Abstract-St}. 

The calculus can be viewed both as a formal axiomatic theory of complementary observables in categorical algebra, and as a symbolic notation for tensor networks representing quantum states/linear operators. Reasoning is purely graphical.
 % 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, in a stunning achievement, 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}.
  
  %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]}}
%  
\TODOb{The figure is especially placed to match the text DON'T CHANGE IT}
The tensor network structure means that the \zxcalculus represents all quantum operations such as 
 initialisation, unitaries, measurements and discarding in a single notation. This notation is significantly 
     \begin{wrapfigure}{r}{0.75\textwidth}
    \vspace*{-8mm}%
%    \texttt{\color{red!70!black} [Placeholder?]} \\[-5ex]
    \hspace*{-4mm}%
    \cgraph[0.7]{circuit-fig}%
    \vspace*{-11mm}  
    \end{wrapfigure}
%\includegraphics[width=\textwidth]{figures/circuit-fig}
more powerful and 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}, as in the adjacent figure:
%An example of such a transformation is the following:

Members of our consortium have demonstrated 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 {outperform
  other methods of circuit optimisation,  minimising certain
  circuit metrics such as total size, tree-width, or number of
 T-gates. Our
industry partner CQC develops \tket, a retargetable quantum compiler
which, using \zx-based optimisations, outperforms all existing
compilers for quantum software.\vspace{-1.5mm}%suck
\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  address the theme of \emph{Quantum Computation}.
We develop tools for running quantum programs
on any available quantum device and benchmarking algorithms and machines, significantly 
enhancing the capabilities of near-term quantum computers.

% speed new quantum devices and architectures into use, and broaden the range of potential users of quantum computers.

\subsection{Novelty, level of ambition and foundational character}\vspace{-1.5mm}%suck
\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.}
}


\paragraph{Novelty:}
\label{sec:novelty}

The concept of a `deep' quantum compiler is entirely novel. Integrating optimisation and error correction intelligently into the stack gives a completely new set of tools for developing and using quantum computers.
  Using the \zxcalculus to manage resources in quantum hardware is a totally new application of the \zxcalculus, and an ambitious new way to realise computations on heterogenous quantum hardware.
%  Unlike sequences of gates, the tensor networks which are the terms of the \zxcalculus have no preordained causal structure beyond the global input and output, helping us to achieve optimal implementations on diverse architectures.
Furthermore, our system allows transformations of tensor networks which cannot be expressed as equations between circuits as illustrated in the figure on the previous page.
  In addition, the \zxcalculus is a sound and complete formal system for transforming quantum procedures, so that each program transformation which our compiler system comes with a proof of its correctness.
  The way that the \zxcalculus represents quantum procedures also avoids the immediate dimensional explosion associated with explicit matrices, so that it will in many cases be more efficient than any other automated technique for reasoning about quantum procedures.
The categorisation of multiple post-classical resources is also novel, as is the incorporation into the compiler chain. The development of a compiler stack that also doubles as a benchmarking tool is entirely new.\vspace{-1.5mm}%suck


\paragraph{Ambition:}
\label{sec:ambition} 

  A ``deep compiler'' for quantum computing systems allows for modular design of the software stack. This lets programmers write at a high level for any hardware and any quantum error correcting codes. It is nevertheless tightly integrated upon compilation. In addition, it is fully tailored to the specific resources, architecture, control systems, and hardware of a specific platform. Furthermore the project includes isolating, integrating, and then certifying quantum speed-up.
  %\texttt{\bfseries \color{red!70!black}[refer to specific platforms here (NQIT + Grenoble)?]}
  This is very technically ambitious: but while it has never been done before, we believe it to be achievable on the basis of our earlier work, and the ideal combination of skills within the project consortium.\vspace{-1.5mm}%suck



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

Deep quantum compilation includes many tools that derive from foundational research.
The \dzxc system will be not just a compiler but also a foundational tool (for example for the characterisation of post-classical resources).
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.
A key example of why this is necessary, exploited by NQIT and others, is that lattice surgery operations on surface codes do not fit into the gate model, but have simple representations in the \zxcalculus \cite{BH-2017}.
The ability to demonstrate quantum speed-up at compile-time will enhance our understanding of what is unique about quantum processing.
The deep quantum compiler we will develop
will do the heavy lifting of managing resources and mapping operations to quantum hardware, %allowing the developers of both hardware and software to focus elsewhere.
%This will 
facilitating the development of new architectures and technologies for quantum computing.




\subsection{Concept and methodology}\vspace{-1.5mm}%suck
\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.
}

The proposed \dzxc (``\emph{deep ZX compilation}'') system is an advanced \textsc{zx}-style system
augmented with features needed for applications.
The \zxcalculus occupies a place in quantum computation similar to the
$\lambda$-calculus in classical computing providing a solid but
austere theoretical foundation. %, without any niceties for practical usage. 
The \dzxc system will augment this basic formal system with a second layer of
\emph{annotations} on the tensor graph, describing program parameters
and architectural constraints of a specific hardware configuration.
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. Further, at this stage
a program can be translated to a fault-tolerant equivalent with
respect to a chosen error-correcting code.
We will also develop translations for the \dzxc system from existing quantum programming languages early in the project.
These will provide
 examples and test cases, and allow comparative
evaluation.



The annotations of the second layer provide the basis of \emph{augmented
  rewrites}: program transformations guided by the
annotations to achieve particular goals. %, not expressible in the basic tensor language.  
For instance, there is an efficient algorithm
\cite{Mhalla:2008kx} to find the \emph{gflow} of a graph state; if the
state has a gflow then it supports deterministic 1-way computation
\cite{D.E.-Browne2007Generalized-Flo}.  Annotating the graph with its
gflow provides guidance for a rewrite strategy which produces an
equivalent, space-optimal circuit \cite{Duncan:2010aa}.
The \dzxc system
 generalises this concept to include other annotation information to inform re-writing. 
% encompass other sorts of information which would inform how to transform (i.e.,~to re-write) a generic representation of a quantum computational procedure.
For example, 
the \dzxc system could incorporate
a system which specifies both how to represent logical operations in a particular error correcting code, and how the operations are constrained in order to satisfy %basic precautions to keep the realisation 
fault-tolerance.

The \dzxc system will be modular, allowing for several different systems of annotations.
The \dzxc system
will re-write procedures, minimising the number of operations, subject to the constraints described by those annotations.
  One such system of annotations will be to describe
the constraints and the costs of operations for particular hardware.
%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, algorithms for inferring
specific annotations, and rewrite strategies which exploit them
form a major novel component of the project.

%The \dzxc system
%can therefore re-write procedures, minimising the number of operations, subject to the constraints described by those annotations.
%
%The \dzxc system will be modular, and allow for several different systems of annotations, for different hardware platforms or constraints one might impose on a computation.
%  One such system of annotations would be to describe
%the constraints and the costs involved for operations within a particular hardware platform (\ref{task:runnable}).
%Augmented
%rewrites will be used to find a runnable implementation of the
%abstract tensor for the target platform, and to optimise resource use.
%The development
%of the general theory of annotations and augmented rewrites
%(\ref{task:annotate1}, \ref{task:annotate2}), algorithms for inferring
%specific annotations (\ref{wp:representation}), and rewrite strategies which exploit them
%(\ref{task:opt-machine}) form a major novel component of the project.%

Concrete tensor networks have a fixed finite size, whereas algorithms
are described in parametric fashion, \eg varying according the
input size.
To use this, the \dzxc system will 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.
While challenging, we have experience of
similar constructs from the \texttt{quantomatic}
project~\cite{KZ:2015:aa, Kissinger2015Quantomatic:-A-}.
\REM{[apropos to refer to PyZX here?]}

A core component in optimising quantum computers is identifying which resources are necessary for non-classical computing. The identification of this quantum speed-up is a live open problem. Drawing on the foundational expressiveness of the \zxcalculus and the expertise in the consortium, and existing automated theorem provers for the calculus, we will identify and express these resources in the \dzxc system.This will enable optimising for use of these resources, and the ability to say at compile time that a procedure is using non-classical processing.
Furthermore, the compiler stack and associated library set of post-classical resources will naturally become a software tool for benchmarking quantum devices, greatly enhancing the maturity of quantum computing technology.

The four major work packages of the project are structured into
various themes: the relation between \zx and other quantum computing representations (\S\ref{sec:progr-lang-supp});  necessary theoretical developments of \zx and the identification of quantum-unique resources (\S\ref{sec:repr-res}); optimisation strategies independent of implementations (\S\ref{sec:indep-opt}); using annotated \zx to compile and optimise for specific hardware (\S\ref{sec:dep-opt}).

\subsubsection{A quantum compiler stack}\vspace{-1.5mm}%suck
\label{sec:progr-lang-supp}


 % 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 interface between multiple different quantum HLLs for quantum procedures, and various hardware platforms.
  This system will use terms of the \zxcalculus as an internal representation of the procedure as it undergoes optimisations and translations, both abstractly and to fit a particular hardware architecture.
%  This representation would not be required from or exposed to the user (although 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, the
  front-end of the \dzxc system 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 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 to a lower-level
  representation, specific to each quantum device.
%
%Proposed and existing quantum devices differ in many ways.
Realistic models of such devices include various restrictions such
as a
fixed number of qubits, bounded total execution time, or
restrictions on which qubits may interact directly.  
%Looking more closely, 
Primitive operations need different amounts of time,
different qubit implementations have different noise models and failure modes,
and low fidelity.
\REM{noise,fidelitY}
%
Due to the novelty of our proposal, we adopt an exploratory approach
to back-end models.  Initially we study
the circuit model and the 1-way
model~\cite{Raussendorf-2001}. %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 
Their similarities and differences allow us
to prototype the development of 
hardware annotations for the \dzxc
system.  In both cases, this
involves: decomposing the tensor network into atomic operations;
 characterising runnability by predicates in monadic second order logic; and
transforming the tensor network into an equivalent runnable version.
This experience will inform the later work in \S\ref{sec:indep-opt} and
\S\ref{sec:dep-opt}.

To encourage interaction from other stakeholder groups, %and to support other languages,  
interfaces for the \dzxc system will be made public.
While we will provide specific modules for the tasks described above, the \dzxc system will be 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
Furthermore, 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 and optimisation techniques.

\subsubsection{Representation, reasoning, and resources}\vspace{-1.5mm}%suck
\label{sec:repr-res}

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

The purpose of the \dzxc system is to form the basis of a compiler, able to generate executables for multiple architectures.
The ability to synthesise hardware-appropriate implementations from abstract descriptions is one of the major novel contributions of this project.
One fundamental problem to address is that of enabling the compiler to optimally use the nonclassical resources that enable quantum processing. 
We carry 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 consists on 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? 
One particular focus is the question of tests based on measurement results: how should they be integrated within the \dzxc system?
We 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.
Aided by the  test suite designed in \S\ref{sec:progr-lang-supp}, this work will enable more sophisticated, generic optimisations to be run in advance of needing any particular computational procedure.
We will also extend the \zx-calculus by (i) expanding it into complete and universal qudit variations to work effectively beyond 2-level systems, 
and (ii) gaining 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. 

Second we will use new results on \zx to identify the nonclassical aspects of quantum theory that enable quantum speed-up, and develop procedures to certify whether a quantum algorithm demonstrates speed-up.
This part of the research 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 from a \zx perspective.
This will further develop \zx as a language to describe quantum theory, and provide insight on outstanding open problems beyond the scope of the current proposal. 
Thirdly, we will tackle the identification of resources for speed-up, via a comparative study of axiomatic representations of different paradigms of computation (such as Clifford and Clifford+T). We will characterise quantum resources in a systematic manner using the \zx framework, and contrast our findings with the current intuitions for sources of quantum speed-up (such as contextuality and Bell nonlocality). The outcome of this work will also include the development of representations 
of contextuality within the \zx language.
Finally, we will develop certification tools for quantum speed-up, by using re-writing processes to identify candidate subroutines that require nonclassical resources to be carried out. 

\subsubsection{Machine-independent optimisation}\vspace{-1.5mm}%suck
\label{sec:indep-opt}

%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.
at the core of this proposal.
%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, 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 \S\ref{sec:progr-lang-supp} or \S\ref{sec:repr-res} using existing techniques (as well as incorporating any further useful techniques developed in \S\ref{sec:repr-res} and this section).

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

We will also provide the \dzxc system with the ability to express topological constraints and causal ordering, such as 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 need for error corrected systems.

The second stage of the compilation process is re-writing generic \zx terms on idealised quantum systems to transformations of error-corrected qubits. Doing this automatically is a major element in deep compilation.
%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, t
%This will also take as input and apply a 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}\vspace{-1.5mm}%suck
\label{sec:dep-opt}

The final, machine-dependent part of the deep compilation process consists of two stages: formatting to the target system and the application of machine-dependent optimisations.
%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.
The main tasks are: to add suitable machine-dependent error protection to the program;  optimise the program according to whichever resources are most appropriate for the given machine; and lay out the program for execution. 
This work package represents the most technically involved and multi-disciplinary component of the project, and requires the integration of the front-end (\S\ref{sec:progr-lang-supp}), the theoretical work of \S\ref{sec:repr-res} and instantiation of the generic optimizations considered in \S\ref{sec:indep-opt}.


We will develop a further layer of annotations for \zx terms representing real-world hardware constraints. %, 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: 
specific hardware technologies: silicon spin qubits (Grenoble), optically linked ion traps (NQIT), and an IBM device (through the CQC team). %in Task~\ref{task:NQIT-model}.
In the first two 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.
This allows \dzxc-generated programs to 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 particular, 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 term which closely models the constraints of a target architecture.
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 to the physical constraints of specific hardware.
%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 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, respecting the constraints of the specific choice of error correction strategy and machine resources specified by the input.
%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 highly optimise the resources used in any particular hardware platform without requiring the use of bespoke techniques for each target architecture.


\subsection{Interdisciplinary nature}\vspace{-1.5mm}%suck
\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 \& Formal Methods} at the high level, through {\textbf{Quantum Physics},} \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 physics from operational compositionality, and} 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 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, \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 foundations, and on to formal methods of computer science.
This \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} for bi-directional knowledge exchange.
The project also involves several other research groups that have been founded in the past few years and links to QuEnG and NQIT, thus \textbf{building leading innovation capacity}.
Additionally, the team includes as PIs and Co-Is multiple \textbf{excellent young researchers}.
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}
The primary means of dissemination will be by publishing our results
in leading journals and conferences.
We will target specialist quantum information venues such as \emph{Quantum Information and Computation} (QIC) or \emph{Quantum Information Processing} (QIP), mainstream computer science venues such as \emph{International Conference on Computer-Aided Design} (ICCAD) or \emph{Logic in Computer Science} (LiCS), and physics journals such as \emph{Physical Review Letters} (PRL) or \emph{New Journal of Physics} (NJP).
We support open access publishing and will aim in particular to publish in diamond open access journals \emph{Quantum} and our own \emph{Compositionality}, as well as 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 and beyond.

\paragraph{Exploitation of results.\!\!}
Through CQC, our research will be integrated with the leading quantum
software compiler system, \tket.
As \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.
The integration with the QuEnG and NQIT projects, through key members (Horsman and de Beaudrap), gives a direct pipeline to technological implementation.
%Furthermore, we will provide a programming framework for the networked quantum computer developed as part of the NQIT project, of which one of our researchers (de Beaudrap) is a key member.
We seek close collaboration with architectures teams, and will show results at the meetings including the UK Quantum Technologies annual showcase.

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

Beyond online self-publishing we will also pitch articles to magazines aimed at a general audience in several languages, such as \emph{Communications of the ACM} and \emph{La Recherche}.



\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),
which will proceed in parallel.  They all contribute to the ultimate goal of providing the full theoretical underpinning as well as the actual realization of deep quantum compilation software, based on \zxcalculus.  The workpackages are:
%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[{\bf WP 1}] is focussed on 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 for benchmarking.
\item[{\bf WP 2}] is focussed on the further development of zx calculus, its axiomatic formulation, and its status as a theory of resources including for quantum speed-up.
%is about modelling the properties of different machines in \azx, and translating \azx to hardware.
\item[{\bf WP 3}] 
focusses on resource optimization, such as gate reduction in circuit representations, efficient intelligent error-correction, and other deep compilation algorithms.
%develops the theory behind \azx and algorithms  to realise the logical ideas.
\item[{\bf WP 4}]
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.  
Our work plan consists of a balance of short tasks with concrete software deliverables and longer term, more ambitious and open-ended tasks which can offer significant, but less predictable, step-changes in the state of the art.

The early tasks of {\bf WP 1} 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 {\bf WP 2} build on a significant existing body of results and techniques for the \zxcalculus and quantum information theory and quantum foundations.
Similarly, several tasks of {\bf WP 3} are based on known results and techniques for the \zxcalculus and rewrite theory in general, so can begin immediately.  The more challenging machine models of {\bf WP 4} are scheduled to begin in parallel with the more challenging theoretical tasks in {\bf WP 3}, anticipating a 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, developing representations for recursion and control, and expressing topological and causal constraints.
Throughout the project, we will check the performance of our methods against competitors and benchmark our software using the open test-suite we will develop.

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

%\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} 
%    & \ref{wp:frontend} 
%    & \ref{wp:representation} 
%    & \ref{wp:theory}
%    & \ref{wp:usefulstuff} 
%    & \ref{wp:admin} 
%    & \textbf{TOTAL} \\\hline
%1. Grenoble   &  12 & 2 & 12 & 20 & 3  & 49 \\\hline
%2. LORIA      & 20 & 12 & 9  & 9  & 3  & 53 \\\hline
%3. Oxford     & 32 & 14 & 30 & 12 & 2  & 90 \\\hline
%4. CQC        &  4 & 0  & 6 &  2 & 0  & 12 \\\hline
%5. Gdansk     &  12& 42 & 12 & 6 & 4  & 76 \\\hline
%6. Nijmegen   &  3 & 6  & 12 & 0 & 0  & 21 \\\hline
%\textbf{TOTAL}& 83 & 76 & 81 & 49 & 12 & 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 work packages will be done
by Horsman/Grenoble, which will also handle project administration. The project will be managed by a senior scientist from each site: 
Coecke (Oxford), Duncan (CQC), Horsman (Grenoble), Sainz (Gdansk),
Perdrix (LORIA), and Kissinger (Nijmegen).  They will track
global progress to ensure milestones are reached.
Each work package will be lead by a responsible PI  
%who will coordinate
%research activity between sites to 
who ensures that deliverables are met:
%achieve WP-specific objectives, and organise collaboration meetings as needed.  
{\bf WP 1}: Perdrix (LORIA), 
{\bf WP 2}: Sainz (Gdansk),
{\bf WP 3}: Coecke (Oxford),
{\bf WP 4}: 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 Prof.~Auffeves, Lead of the
Grenoble Quantum Engineering project, and Prof.~Vinet, head of the silicon spin qubit experimental team,  as external advisors. 
%Prof. Auffeves is the , 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.

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

The milestones are as follows:
\begin{description} 
\item[{\bf M1}] Minimal QASM $\to$ QASM circuit optimiser (month 12)
\item[{\bf M2}] Support for one HLL using parametric \zx, with 1WQC and idealized circuit output (month 18)
\item[{\bf M3}] Architecture sensitive, fidelity aware optimiser \& error correction support (month 24)
\item[{\bf M4}] Back-end support for Oxford Ion Traps, initial back end API (month 30)
\item[{\bf M5}] Complete deep-\zx compiler stack with open
APIs, and a target compiled protocol demonstrating explicit quantum speed-up. (month 36)
\end{description}
Hence, 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.  

We have sufficient proof-of concept results to guaranty that the major components of this proposal will be successful.  It's modular nature moreover means that not achieving maximal gain in one component won't affect the feasibility of the project as a whole. We are very sure that the final goal is achievable, although the effort required for some components may be somewhat uncertain, but with a large flexible team like ours this is a risk that can be easily overcome. 

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